(0) Obligation:

Clauses:

delete(X, tree(X, void, Right), Right).
delete(X, tree(X, Left, void), Left).
delete(X, tree(X, Left, Right), tree(Y, Left, Right1)) :- delmin(Right, Y, Right1).
delete(X, tree(Y, Left, Right), tree(Y, Left1, Right)) :- ','(less(X, Y), delete(X, Left, Left1)).
delete(X, tree(Y, Left, Right), tree(Y, Left, Right1)) :- ','(less(Y, X), delete(X, Right, Right1)).
delmin(tree(Y, void, Right), Y, Right).
delmin(tree(X, Left, X1), Y, tree(X, Left1, X2)) :- delmin(Left, Y, Left1).
less(0, s(X3)).
less(s(X), s(Y)) :- less(X, Y).

Query: delete(g,g,a)

(1) PrologToPrologProblemTransformerProof (SOUND transformation)

Built Prolog problem from termination graph ICLP10.

(2) Obligation:

Clauses:

lessA(s(T31)) :- lessA(T31).
pB(T26, T28) :- lessA(T26).
pB(T26, T28) :- ','(lessA(T26), deleteC(T26, void, T28)).
pD(T50, T45) :- lessA(T50).
pD(T50, T45) :- ','(lessA(T50), deleteC(s(T50), void, T45)).
delminE(tree(T132, void, T133), T132, T133).
delminE(tree(T146, T147, T148), T152, tree(T146, T153, T151)) :- delminE(T147, T152, T153).
pF(T180, T181, T183) :- lessA(T180).
pF(T180, T181, T183) :- ','(lessA(T180), deleteC(T180, T181, T183)).
lessG(0, s(T539)).
lessG(s(T544), s(T545)) :- lessG(T544, T545).
lessH(0, s(T444)).
lessH(s(0), s(s(T457))).
lessH(s(s(0)), s(s(s(T470)))).
lessH(s(s(s(0))), s(s(s(s(T483))))).
lessH(s(s(s(s(0)))), s(s(s(s(s(T496)))))).
lessH(s(s(s(s(s(0))))), s(s(s(s(s(s(T509))))))).
lessH(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T522)))))))).
lessH(s(s(s(s(s(s(s(T527))))))), s(s(s(s(s(s(s(T528)))))))) :- lessG(T527, T528).
deleteC(T6, tree(T6, void, T7), T7).
deleteC(T9, tree(T9, void, void), void).
deleteC(T26, tree(T26, void, void), tree(T26, T28, void)) :- pB(T26, T28).
deleteC(T38, tree(T38, void, void), tree(T38, void, T40)) :- pB(T38, T40).
deleteC(s(T50), tree(s(T50), void, void), tree(s(T50), T45, void)) :- pD(T50, T45).
deleteC(T57, tree(T57, void, void), tree(T57, void, T59)) :- pB(T57, T59).
deleteC(s(T67), tree(s(T67), void, void), tree(s(T67), void, T64)) :- pD(T67, T64).
deleteC(T72, tree(T72, void, tree(T86, void, T87)), tree(T86, void, T87)).
deleteC(T72, tree(T72, void, tree(T112, T113, T114)), tree(T118, void, tree(T112, T119, T117))) :- delminE(T113, T118, T119).
deleteC(T170, tree(T170, void, T171), tree(T170, T173, T171)) :- pB(T170, T173).
deleteC(T180, tree(T180, void, T181), tree(T180, void, T183)) :- pF(T180, T181, T183).
deleteC(s(T199), tree(s(T199), void, T192), tree(s(T199), T194, T192)) :- lessA(T199).
deleteC(s(T199), tree(s(T199), void, T192), tree(s(T199), T194, T192)) :- ','(lessA(T199), deleteC(s(T199), void, T194)).
deleteC(T208, tree(T208, void, T209), tree(T208, void, T211)) :- pF(T208, T209, T211).
deleteC(s(T221), tree(s(T221), void, T216), tree(s(T221), void, T218)) :- lessA(T221).
deleteC(s(T221), tree(s(T221), void, T216), tree(s(T221), void, T218)) :- ','(lessA(T221), deleteC(s(T221), T216, T218)).
deleteC(T228, tree(T228, T229, void), T229).
deleteC(T252, tree(T252, T253, void), tree(T252, T255, void)) :- lessA(T252).
deleteC(T252, tree(T252, T253, void), tree(T252, T255, void)) :- ','(lessA(T252), deleteC(T252, T253, T255)).
deleteC(T266, tree(T266, T267, void), tree(T266, T267, T269)) :- pB(T266, T269).
deleteC(s(T281), tree(s(T281), T274, void), tree(s(T281), T276, void)) :- lessA(T281).
deleteC(s(T281), tree(s(T281), T274, void), tree(s(T281), T276, void)) :- ','(lessA(T281), deleteC(s(T281), T274, T276)).
deleteC(T292, tree(T292, T293, void), tree(T292, T293, T295)) :- pB(T292, T295).
deleteC(s(T305), tree(s(T305), T300, void), tree(s(T305), T300, T302)) :- lessA(T305).
deleteC(s(T305), tree(s(T305), T300, void), tree(s(T305), T300, T302)) :- ','(lessA(T305), deleteC(s(T305), void, T302)).
deleteC(T313, tree(T313, T314, tree(T328, void, T329)), tree(T328, T314, T329)).
deleteC(T313, tree(T313, T314, tree(T354, T355, T356)), tree(T360, T314, tree(T354, T361, T359))) :- delminE(T355, T360, T361).
deleteC(T382, tree(T382, T383, T384), tree(T382, T386, T384)) :- lessA(T382).
deleteC(T382, tree(T382, T383, T384), tree(T382, T386, T384)) :- ','(lessA(T382), deleteC(T382, T383, T386)).
deleteC(T399, tree(T399, T400, T401), tree(T399, T400, T403)) :- lessA(T399).
deleteC(T399, tree(T399, T400, T401), tree(T399, T400, T403)) :- ','(lessA(T399), deleteC(T399, T401, T403)).
deleteC(0, tree(s(T423), T415, T416), tree(s(T423), T418, T416)) :- deleteC(0, T415, T418).
deleteC(s(T434), tree(s(T435), T415, T416), tree(s(T435), T418, T416)) :- lessH(T434, T435).
deleteC(s(T434), tree(s(T435), T415, T416), tree(s(T435), T418, T416)) :- ','(lessH(T434, T435), deleteC(s(T434), T415, T418)).
deleteC(T562, tree(T563, T564, T565), tree(T563, T564, T567)) :- lessG(T563, T562).
deleteC(T562, tree(T563, T564, T565), tree(T563, T564, T567)) :- ','(lessG(T563, T562), deleteC(T562, T565, T567)).
deleteC(s(T591), tree(0, T583, T584), tree(0, T583, T586)) :- deleteC(s(T591), T584, T586).
deleteC(s(T601), tree(s(T600), T583, T584), tree(s(T600), T583, T586)) :- lessG(T600, T601).
deleteC(s(T601), tree(s(T600), T583, T584), tree(s(T600), T583, T586)) :- ','(lessG(T600, T601), deleteC(s(T601), T584, T586)).

Query: deleteC(g,g,a)

(3) PrologToPiTRSProof (SOUND transformation)

We use the technique of [TOCL09]. With regard to the inferred argument filtering the predicates were used in the following modes:
deleteC_in: (b,b,f)
pB_in: (b,f)
lessA_in: (b)
pD_in: (b,f)
delminE_in: (b,f,f)
pF_in: (b,b,f)
lessH_in: (b,b)
lessG_in: (b,b)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

deleteC_in_gga(T6, tree(T6, void, T7), T7) → deleteC_out_gga(T6, tree(T6, void, T7), T7)
deleteC_in_gga(T9, tree(T9, void, void), void) → deleteC_out_gga(T9, tree(T9, void, void), void)
deleteC_in_gga(T26, tree(T26, void, void), tree(T26, T28, void)) → U11_gga(T26, T28, pB_in_ga(T26, T28))
pB_in_ga(T26, T28) → U2_ga(T26, T28, lessA_in_g(T26))
lessA_in_g(s(T31)) → U1_g(T31, lessA_in_g(T31))
U1_g(T31, lessA_out_g(T31)) → lessA_out_g(s(T31))
U2_ga(T26, T28, lessA_out_g(T26)) → pB_out_ga(T26, T28)
U2_ga(T26, T28, lessA_out_g(T26)) → U3_ga(T26, T28, deleteC_in_gga(T26, void, T28))
deleteC_in_gga(T38, tree(T38, void, void), tree(T38, void, T40)) → U12_gga(T38, T40, pB_in_ga(T38, T40))
U12_gga(T38, T40, pB_out_ga(T38, T40)) → deleteC_out_gga(T38, tree(T38, void, void), tree(T38, void, T40))
deleteC_in_gga(s(T50), tree(s(T50), void, void), tree(s(T50), T45, void)) → U13_gga(T50, T45, pD_in_ga(T50, T45))
pD_in_ga(T50, T45) → U4_ga(T50, T45, lessA_in_g(T50))
U4_ga(T50, T45, lessA_out_g(T50)) → pD_out_ga(T50, T45)
U4_ga(T50, T45, lessA_out_g(T50)) → U5_ga(T50, T45, deleteC_in_gga(s(T50), void, T45))
deleteC_in_gga(T57, tree(T57, void, void), tree(T57, void, T59)) → U14_gga(T57, T59, pB_in_ga(T57, T59))
U14_gga(T57, T59, pB_out_ga(T57, T59)) → deleteC_out_gga(T57, tree(T57, void, void), tree(T57, void, T59))
deleteC_in_gga(s(T67), tree(s(T67), void, void), tree(s(T67), void, T64)) → U15_gga(T67, T64, pD_in_ga(T67, T64))
U15_gga(T67, T64, pD_out_ga(T67, T64)) → deleteC_out_gga(s(T67), tree(s(T67), void, void), tree(s(T67), void, T64))
deleteC_in_gga(T72, tree(T72, void, tree(T86, void, T87)), tree(T86, void, T87)) → deleteC_out_gga(T72, tree(T72, void, tree(T86, void, T87)), tree(T86, void, T87))
deleteC_in_gga(T72, tree(T72, void, tree(T112, T113, T114)), tree(T118, void, tree(T112, T119, T117))) → U16_gga(T72, T112, T113, T114, T118, T119, T117, delminE_in_gaa(T113, T118, T119))
delminE_in_gaa(tree(T132, void, T133), T132, T133) → delminE_out_gaa(tree(T132, void, T133), T132, T133)
delminE_in_gaa(tree(T146, T147, T148), T152, tree(T146, T153, T151)) → U6_gaa(T146, T147, T148, T152, T153, T151, delminE_in_gaa(T147, T152, T153))
U6_gaa(T146, T147, T148, T152, T153, T151, delminE_out_gaa(T147, T152, T153)) → delminE_out_gaa(tree(T146, T147, T148), T152, tree(T146, T153, T151))
U16_gga(T72, T112, T113, T114, T118, T119, T117, delminE_out_gaa(T113, T118, T119)) → deleteC_out_gga(T72, tree(T72, void, tree(T112, T113, T114)), tree(T118, void, tree(T112, T119, T117)))
deleteC_in_gga(T170, tree(T170, void, T171), tree(T170, T173, T171)) → U17_gga(T170, T171, T173, pB_in_ga(T170, T173))
U17_gga(T170, T171, T173, pB_out_ga(T170, T173)) → deleteC_out_gga(T170, tree(T170, void, T171), tree(T170, T173, T171))
deleteC_in_gga(T180, tree(T180, void, T181), tree(T180, void, T183)) → U18_gga(T180, T181, T183, pF_in_gga(T180, T181, T183))
pF_in_gga(T180, T181, T183) → U7_gga(T180, T181, T183, lessA_in_g(T180))
U7_gga(T180, T181, T183, lessA_out_g(T180)) → pF_out_gga(T180, T181, T183)
U7_gga(T180, T181, T183, lessA_out_g(T180)) → U8_gga(T180, T181, T183, deleteC_in_gga(T180, T181, T183))
deleteC_in_gga(s(T199), tree(s(T199), void, T192), tree(s(T199), T194, T192)) → U19_gga(T199, T192, T194, lessA_in_g(T199))
U19_gga(T199, T192, T194, lessA_out_g(T199)) → deleteC_out_gga(s(T199), tree(s(T199), void, T192), tree(s(T199), T194, T192))
U19_gga(T199, T192, T194, lessA_out_g(T199)) → U20_gga(T199, T192, T194, deleteC_in_gga(s(T199), void, T194))
deleteC_in_gga(T208, tree(T208, void, T209), tree(T208, void, T211)) → U21_gga(T208, T209, T211, pF_in_gga(T208, T209, T211))
U21_gga(T208, T209, T211, pF_out_gga(T208, T209, T211)) → deleteC_out_gga(T208, tree(T208, void, T209), tree(T208, void, T211))
deleteC_in_gga(s(T221), tree(s(T221), void, T216), tree(s(T221), void, T218)) → U22_gga(T221, T216, T218, lessA_in_g(T221))
U22_gga(T221, T216, T218, lessA_out_g(T221)) → deleteC_out_gga(s(T221), tree(s(T221), void, T216), tree(s(T221), void, T218))
U22_gga(T221, T216, T218, lessA_out_g(T221)) → U23_gga(T221, T216, T218, deleteC_in_gga(s(T221), T216, T218))
deleteC_in_gga(T228, tree(T228, T229, void), T229) → deleteC_out_gga(T228, tree(T228, T229, void), T229)
deleteC_in_gga(T252, tree(T252, T253, void), tree(T252, T255, void)) → U24_gga(T252, T253, T255, lessA_in_g(T252))
U24_gga(T252, T253, T255, lessA_out_g(T252)) → deleteC_out_gga(T252, tree(T252, T253, void), tree(T252, T255, void))
U24_gga(T252, T253, T255, lessA_out_g(T252)) → U25_gga(T252, T253, T255, deleteC_in_gga(T252, T253, T255))
deleteC_in_gga(T266, tree(T266, T267, void), tree(T266, T267, T269)) → U26_gga(T266, T267, T269, pB_in_ga(T266, T269))
U26_gga(T266, T267, T269, pB_out_ga(T266, T269)) → deleteC_out_gga(T266, tree(T266, T267, void), tree(T266, T267, T269))
deleteC_in_gga(s(T281), tree(s(T281), T274, void), tree(s(T281), T276, void)) → U27_gga(T281, T274, T276, lessA_in_g(T281))
U27_gga(T281, T274, T276, lessA_out_g(T281)) → deleteC_out_gga(s(T281), tree(s(T281), T274, void), tree(s(T281), T276, void))
U27_gga(T281, T274, T276, lessA_out_g(T281)) → U28_gga(T281, T274, T276, deleteC_in_gga(s(T281), T274, T276))
deleteC_in_gga(T292, tree(T292, T293, void), tree(T292, T293, T295)) → U29_gga(T292, T293, T295, pB_in_ga(T292, T295))
U29_gga(T292, T293, T295, pB_out_ga(T292, T295)) → deleteC_out_gga(T292, tree(T292, T293, void), tree(T292, T293, T295))
deleteC_in_gga(s(T305), tree(s(T305), T300, void), tree(s(T305), T300, T302)) → U30_gga(T305, T300, T302, lessA_in_g(T305))
U30_gga(T305, T300, T302, lessA_out_g(T305)) → deleteC_out_gga(s(T305), tree(s(T305), T300, void), tree(s(T305), T300, T302))
U30_gga(T305, T300, T302, lessA_out_g(T305)) → U31_gga(T305, T300, T302, deleteC_in_gga(s(T305), void, T302))
deleteC_in_gga(T313, tree(T313, T314, tree(T328, void, T329)), tree(T328, T314, T329)) → deleteC_out_gga(T313, tree(T313, T314, tree(T328, void, T329)), tree(T328, T314, T329))
deleteC_in_gga(T313, tree(T313, T314, tree(T354, T355, T356)), tree(T360, T314, tree(T354, T361, T359))) → U32_gga(T313, T314, T354, T355, T356, T360, T361, T359, delminE_in_gaa(T355, T360, T361))
U32_gga(T313, T314, T354, T355, T356, T360, T361, T359, delminE_out_gaa(T355, T360, T361)) → deleteC_out_gga(T313, tree(T313, T314, tree(T354, T355, T356)), tree(T360, T314, tree(T354, T361, T359)))
deleteC_in_gga(T382, tree(T382, T383, T384), tree(T382, T386, T384)) → U33_gga(T382, T383, T384, T386, lessA_in_g(T382))
U33_gga(T382, T383, T384, T386, lessA_out_g(T382)) → deleteC_out_gga(T382, tree(T382, T383, T384), tree(T382, T386, T384))
U33_gga(T382, T383, T384, T386, lessA_out_g(T382)) → U34_gga(T382, T383, T384, T386, deleteC_in_gga(T382, T383, T386))
deleteC_in_gga(T399, tree(T399, T400, T401), tree(T399, T400, T403)) → U35_gga(T399, T400, T401, T403, lessA_in_g(T399))
U35_gga(T399, T400, T401, T403, lessA_out_g(T399)) → deleteC_out_gga(T399, tree(T399, T400, T401), tree(T399, T400, T403))
U35_gga(T399, T400, T401, T403, lessA_out_g(T399)) → U36_gga(T399, T400, T401, T403, deleteC_in_gga(T399, T401, T403))
deleteC_in_gga(0, tree(s(T423), T415, T416), tree(s(T423), T418, T416)) → U37_gga(T423, T415, T416, T418, deleteC_in_gga(0, T415, T418))
deleteC_in_gga(s(T434), tree(s(T435), T415, T416), tree(s(T435), T418, T416)) → U38_gga(T434, T435, T415, T416, T418, lessH_in_gg(T434, T435))
lessH_in_gg(0, s(T444)) → lessH_out_gg(0, s(T444))
lessH_in_gg(s(0), s(s(T457))) → lessH_out_gg(s(0), s(s(T457)))
lessH_in_gg(s(s(0)), s(s(s(T470)))) → lessH_out_gg(s(s(0)), s(s(s(T470))))
lessH_in_gg(s(s(s(0))), s(s(s(s(T483))))) → lessH_out_gg(s(s(s(0))), s(s(s(s(T483)))))
lessH_in_gg(s(s(s(s(0)))), s(s(s(s(s(T496)))))) → lessH_out_gg(s(s(s(s(0)))), s(s(s(s(s(T496))))))
lessH_in_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T509))))))) → lessH_out_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T509)))))))
lessH_in_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T522)))))))) → lessH_out_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T522))))))))
lessH_in_gg(s(s(s(s(s(s(s(T527))))))), s(s(s(s(s(s(s(T528)))))))) → U10_gg(T527, T528, lessG_in_gg(T527, T528))
lessG_in_gg(0, s(T539)) → lessG_out_gg(0, s(T539))
lessG_in_gg(s(T544), s(T545)) → U9_gg(T544, T545, lessG_in_gg(T544, T545))
U9_gg(T544, T545, lessG_out_gg(T544, T545)) → lessG_out_gg(s(T544), s(T545))
U10_gg(T527, T528, lessG_out_gg(T527, T528)) → lessH_out_gg(s(s(s(s(s(s(s(T527))))))), s(s(s(s(s(s(s(T528))))))))
U38_gga(T434, T435, T415, T416, T418, lessH_out_gg(T434, T435)) → deleteC_out_gga(s(T434), tree(s(T435), T415, T416), tree(s(T435), T418, T416))
U38_gga(T434, T435, T415, T416, T418, lessH_out_gg(T434, T435)) → U39_gga(T434, T435, T415, T416, T418, deleteC_in_gga(s(T434), T415, T418))
deleteC_in_gga(T562, tree(T563, T564, T565), tree(T563, T564, T567)) → U40_gga(T562, T563, T564, T565, T567, lessG_in_gg(T563, T562))
U40_gga(T562, T563, T564, T565, T567, lessG_out_gg(T563, T562)) → deleteC_out_gga(T562, tree(T563, T564, T565), tree(T563, T564, T567))
U40_gga(T562, T563, T564, T565, T567, lessG_out_gg(T563, T562)) → U41_gga(T562, T563, T564, T565, T567, deleteC_in_gga(T562, T565, T567))
deleteC_in_gga(s(T591), tree(0, T583, T584), tree(0, T583, T586)) → U42_gga(T591, T583, T584, T586, deleteC_in_gga(s(T591), T584, T586))
deleteC_in_gga(s(T601), tree(s(T600), T583, T584), tree(s(T600), T583, T586)) → U43_gga(T601, T600, T583, T584, T586, lessG_in_gg(T600, T601))
U43_gga(T601, T600, T583, T584, T586, lessG_out_gg(T600, T601)) → deleteC_out_gga(s(T601), tree(s(T600), T583, T584), tree(s(T600), T583, T586))
U43_gga(T601, T600, T583, T584, T586, lessG_out_gg(T600, T601)) → U44_gga(T601, T600, T583, T584, T586, deleteC_in_gga(s(T601), T584, T586))
U44_gga(T601, T600, T583, T584, T586, deleteC_out_gga(s(T601), T584, T586)) → deleteC_out_gga(s(T601), tree(s(T600), T583, T584), tree(s(T600), T583, T586))
U42_gga(T591, T583, T584, T586, deleteC_out_gga(s(T591), T584, T586)) → deleteC_out_gga(s(T591), tree(0, T583, T584), tree(0, T583, T586))
U41_gga(T562, T563, T564, T565, T567, deleteC_out_gga(T562, T565, T567)) → deleteC_out_gga(T562, tree(T563, T564, T565), tree(T563, T564, T567))
U39_gga(T434, T435, T415, T416, T418, deleteC_out_gga(s(T434), T415, T418)) → deleteC_out_gga(s(T434), tree(s(T435), T415, T416), tree(s(T435), T418, T416))
U37_gga(T423, T415, T416, T418, deleteC_out_gga(0, T415, T418)) → deleteC_out_gga(0, tree(s(T423), T415, T416), tree(s(T423), T418, T416))
U36_gga(T399, T400, T401, T403, deleteC_out_gga(T399, T401, T403)) → deleteC_out_gga(T399, tree(T399, T400, T401), tree(T399, T400, T403))
U34_gga(T382, T383, T384, T386, deleteC_out_gga(T382, T383, T386)) → deleteC_out_gga(T382, tree(T382, T383, T384), tree(T382, T386, T384))
U31_gga(T305, T300, T302, deleteC_out_gga(s(T305), void, T302)) → deleteC_out_gga(s(T305), tree(s(T305), T300, void), tree(s(T305), T300, T302))
U28_gga(T281, T274, T276, deleteC_out_gga(s(T281), T274, T276)) → deleteC_out_gga(s(T281), tree(s(T281), T274, void), tree(s(T281), T276, void))
U25_gga(T252, T253, T255, deleteC_out_gga(T252, T253, T255)) → deleteC_out_gga(T252, tree(T252, T253, void), tree(T252, T255, void))
U23_gga(T221, T216, T218, deleteC_out_gga(s(T221), T216, T218)) → deleteC_out_gga(s(T221), tree(s(T221), void, T216), tree(s(T221), void, T218))
U20_gga(T199, T192, T194, deleteC_out_gga(s(T199), void, T194)) → deleteC_out_gga(s(T199), tree(s(T199), void, T192), tree(s(T199), T194, T192))
U8_gga(T180, T181, T183, deleteC_out_gga(T180, T181, T183)) → pF_out_gga(T180, T181, T183)
U18_gga(T180, T181, T183, pF_out_gga(T180, T181, T183)) → deleteC_out_gga(T180, tree(T180, void, T181), tree(T180, void, T183))
U5_ga(T50, T45, deleteC_out_gga(s(T50), void, T45)) → pD_out_ga(T50, T45)
U13_gga(T50, T45, pD_out_ga(T50, T45)) → deleteC_out_gga(s(T50), tree(s(T50), void, void), tree(s(T50), T45, void))
U3_ga(T26, T28, deleteC_out_gga(T26, void, T28)) → pB_out_ga(T26, T28)
U11_gga(T26, T28, pB_out_ga(T26, T28)) → deleteC_out_gga(T26, tree(T26, void, void), tree(T26, T28, void))

The argument filtering Pi contains the following mapping:
deleteC_in_gga(x1, x2, x3)  =  deleteC_in_gga(x1, x2)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
void  =  void
deleteC_out_gga(x1, x2, x3)  =  deleteC_out_gga
U11_gga(x1, x2, x3)  =  U11_gga(x3)
pB_in_ga(x1, x2)  =  pB_in_ga(x1)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
lessA_in_g(x1)  =  lessA_in_g(x1)
s(x1)  =  s(x1)
U1_g(x1, x2)  =  U1_g(x2)
lessA_out_g(x1)  =  lessA_out_g
pB_out_ga(x1, x2)  =  pB_out_ga
U3_ga(x1, x2, x3)  =  U3_ga(x3)
U12_gga(x1, x2, x3)  =  U12_gga(x3)
U13_gga(x1, x2, x3)  =  U13_gga(x3)
pD_in_ga(x1, x2)  =  pD_in_ga(x1)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
pD_out_ga(x1, x2)  =  pD_out_ga
U5_ga(x1, x2, x3)  =  U5_ga(x3)
U14_gga(x1, x2, x3)  =  U14_gga(x3)
U15_gga(x1, x2, x3)  =  U15_gga(x3)
U16_gga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U16_gga(x8)
delminE_in_gaa(x1, x2, x3)  =  delminE_in_gaa(x1)
delminE_out_gaa(x1, x2, x3)  =  delminE_out_gaa(x2)
U6_gaa(x1, x2, x3, x4, x5, x6, x7)  =  U6_gaa(x7)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x4)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x4)
pF_in_gga(x1, x2, x3)  =  pF_in_gga(x1, x2)
U7_gga(x1, x2, x3, x4)  =  U7_gga(x1, x2, x4)
pF_out_gga(x1, x2, x3)  =  pF_out_gga
U8_gga(x1, x2, x3, x4)  =  U8_gga(x4)
U19_gga(x1, x2, x3, x4)  =  U19_gga(x1, x4)
U20_gga(x1, x2, x3, x4)  =  U20_gga(x4)
U21_gga(x1, x2, x3, x4)  =  U21_gga(x4)
U22_gga(x1, x2, x3, x4)  =  U22_gga(x1, x2, x4)
U23_gga(x1, x2, x3, x4)  =  U23_gga(x4)
U24_gga(x1, x2, x3, x4)  =  U24_gga(x1, x2, x4)
U25_gga(x1, x2, x3, x4)  =  U25_gga(x4)
U26_gga(x1, x2, x3, x4)  =  U26_gga(x4)
U27_gga(x1, x2, x3, x4)  =  U27_gga(x1, x2, x4)
U28_gga(x1, x2, x3, x4)  =  U28_gga(x4)
U29_gga(x1, x2, x3, x4)  =  U29_gga(x4)
U30_gga(x1, x2, x3, x4)  =  U30_gga(x1, x4)
U31_gga(x1, x2, x3, x4)  =  U31_gga(x4)
U32_gga(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U32_gga(x9)
U33_gga(x1, x2, x3, x4, x5)  =  U33_gga(x1, x2, x5)
U34_gga(x1, x2, x3, x4, x5)  =  U34_gga(x5)
U35_gga(x1, x2, x3, x4, x5)  =  U35_gga(x1, x3, x5)
U36_gga(x1, x2, x3, x4, x5)  =  U36_gga(x5)
0  =  0
U37_gga(x1, x2, x3, x4, x5)  =  U37_gga(x5)
U38_gga(x1, x2, x3, x4, x5, x6)  =  U38_gga(x1, x3, x6)
lessH_in_gg(x1, x2)  =  lessH_in_gg(x1, x2)
lessH_out_gg(x1, x2)  =  lessH_out_gg
U10_gg(x1, x2, x3)  =  U10_gg(x3)
lessG_in_gg(x1, x2)  =  lessG_in_gg(x1, x2)
lessG_out_gg(x1, x2)  =  lessG_out_gg
U9_gg(x1, x2, x3)  =  U9_gg(x3)
U39_gga(x1, x2, x3, x4, x5, x6)  =  U39_gga(x6)
U40_gga(x1, x2, x3, x4, x5, x6)  =  U40_gga(x1, x4, x6)
U41_gga(x1, x2, x3, x4, x5, x6)  =  U41_gga(x6)
U42_gga(x1, x2, x3, x4, x5)  =  U42_gga(x5)
U43_gga(x1, x2, x3, x4, x5, x6)  =  U43_gga(x1, x4, x6)
U44_gga(x1, x2, x3, x4, x5, x6)  =  U44_gga(x6)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(4) Obligation:

Pi-finite rewrite system:
The TRS R consists of the following rules:

deleteC_in_gga(T6, tree(T6, void, T7), T7) → deleteC_out_gga(T6, tree(T6, void, T7), T7)
deleteC_in_gga(T9, tree(T9, void, void), void) → deleteC_out_gga(T9, tree(T9, void, void), void)
deleteC_in_gga(T26, tree(T26, void, void), tree(T26, T28, void)) → U11_gga(T26, T28, pB_in_ga(T26, T28))
pB_in_ga(T26, T28) → U2_ga(T26, T28, lessA_in_g(T26))
lessA_in_g(s(T31)) → U1_g(T31, lessA_in_g(T31))
U1_g(T31, lessA_out_g(T31)) → lessA_out_g(s(T31))
U2_ga(T26, T28, lessA_out_g(T26)) → pB_out_ga(T26, T28)
U2_ga(T26, T28, lessA_out_g(T26)) → U3_ga(T26, T28, deleteC_in_gga(T26, void, T28))
deleteC_in_gga(T38, tree(T38, void, void), tree(T38, void, T40)) → U12_gga(T38, T40, pB_in_ga(T38, T40))
U12_gga(T38, T40, pB_out_ga(T38, T40)) → deleteC_out_gga(T38, tree(T38, void, void), tree(T38, void, T40))
deleteC_in_gga(s(T50), tree(s(T50), void, void), tree(s(T50), T45, void)) → U13_gga(T50, T45, pD_in_ga(T50, T45))
pD_in_ga(T50, T45) → U4_ga(T50, T45, lessA_in_g(T50))
U4_ga(T50, T45, lessA_out_g(T50)) → pD_out_ga(T50, T45)
U4_ga(T50, T45, lessA_out_g(T50)) → U5_ga(T50, T45, deleteC_in_gga(s(T50), void, T45))
deleteC_in_gga(T57, tree(T57, void, void), tree(T57, void, T59)) → U14_gga(T57, T59, pB_in_ga(T57, T59))
U14_gga(T57, T59, pB_out_ga(T57, T59)) → deleteC_out_gga(T57, tree(T57, void, void), tree(T57, void, T59))
deleteC_in_gga(s(T67), tree(s(T67), void, void), tree(s(T67), void, T64)) → U15_gga(T67, T64, pD_in_ga(T67, T64))
U15_gga(T67, T64, pD_out_ga(T67, T64)) → deleteC_out_gga(s(T67), tree(s(T67), void, void), tree(s(T67), void, T64))
deleteC_in_gga(T72, tree(T72, void, tree(T86, void, T87)), tree(T86, void, T87)) → deleteC_out_gga(T72, tree(T72, void, tree(T86, void, T87)), tree(T86, void, T87))
deleteC_in_gga(T72, tree(T72, void, tree(T112, T113, T114)), tree(T118, void, tree(T112, T119, T117))) → U16_gga(T72, T112, T113, T114, T118, T119, T117, delminE_in_gaa(T113, T118, T119))
delminE_in_gaa(tree(T132, void, T133), T132, T133) → delminE_out_gaa(tree(T132, void, T133), T132, T133)
delminE_in_gaa(tree(T146, T147, T148), T152, tree(T146, T153, T151)) → U6_gaa(T146, T147, T148, T152, T153, T151, delminE_in_gaa(T147, T152, T153))
U6_gaa(T146, T147, T148, T152, T153, T151, delminE_out_gaa(T147, T152, T153)) → delminE_out_gaa(tree(T146, T147, T148), T152, tree(T146, T153, T151))
U16_gga(T72, T112, T113, T114, T118, T119, T117, delminE_out_gaa(T113, T118, T119)) → deleteC_out_gga(T72, tree(T72, void, tree(T112, T113, T114)), tree(T118, void, tree(T112, T119, T117)))
deleteC_in_gga(T170, tree(T170, void, T171), tree(T170, T173, T171)) → U17_gga(T170, T171, T173, pB_in_ga(T170, T173))
U17_gga(T170, T171, T173, pB_out_ga(T170, T173)) → deleteC_out_gga(T170, tree(T170, void, T171), tree(T170, T173, T171))
deleteC_in_gga(T180, tree(T180, void, T181), tree(T180, void, T183)) → U18_gga(T180, T181, T183, pF_in_gga(T180, T181, T183))
pF_in_gga(T180, T181, T183) → U7_gga(T180, T181, T183, lessA_in_g(T180))
U7_gga(T180, T181, T183, lessA_out_g(T180)) → pF_out_gga(T180, T181, T183)
U7_gga(T180, T181, T183, lessA_out_g(T180)) → U8_gga(T180, T181, T183, deleteC_in_gga(T180, T181, T183))
deleteC_in_gga(s(T199), tree(s(T199), void, T192), tree(s(T199), T194, T192)) → U19_gga(T199, T192, T194, lessA_in_g(T199))
U19_gga(T199, T192, T194, lessA_out_g(T199)) → deleteC_out_gga(s(T199), tree(s(T199), void, T192), tree(s(T199), T194, T192))
U19_gga(T199, T192, T194, lessA_out_g(T199)) → U20_gga(T199, T192, T194, deleteC_in_gga(s(T199), void, T194))
deleteC_in_gga(T208, tree(T208, void, T209), tree(T208, void, T211)) → U21_gga(T208, T209, T211, pF_in_gga(T208, T209, T211))
U21_gga(T208, T209, T211, pF_out_gga(T208, T209, T211)) → deleteC_out_gga(T208, tree(T208, void, T209), tree(T208, void, T211))
deleteC_in_gga(s(T221), tree(s(T221), void, T216), tree(s(T221), void, T218)) → U22_gga(T221, T216, T218, lessA_in_g(T221))
U22_gga(T221, T216, T218, lessA_out_g(T221)) → deleteC_out_gga(s(T221), tree(s(T221), void, T216), tree(s(T221), void, T218))
U22_gga(T221, T216, T218, lessA_out_g(T221)) → U23_gga(T221, T216, T218, deleteC_in_gga(s(T221), T216, T218))
deleteC_in_gga(T228, tree(T228, T229, void), T229) → deleteC_out_gga(T228, tree(T228, T229, void), T229)
deleteC_in_gga(T252, tree(T252, T253, void), tree(T252, T255, void)) → U24_gga(T252, T253, T255, lessA_in_g(T252))
U24_gga(T252, T253, T255, lessA_out_g(T252)) → deleteC_out_gga(T252, tree(T252, T253, void), tree(T252, T255, void))
U24_gga(T252, T253, T255, lessA_out_g(T252)) → U25_gga(T252, T253, T255, deleteC_in_gga(T252, T253, T255))
deleteC_in_gga(T266, tree(T266, T267, void), tree(T266, T267, T269)) → U26_gga(T266, T267, T269, pB_in_ga(T266, T269))
U26_gga(T266, T267, T269, pB_out_ga(T266, T269)) → deleteC_out_gga(T266, tree(T266, T267, void), tree(T266, T267, T269))
deleteC_in_gga(s(T281), tree(s(T281), T274, void), tree(s(T281), T276, void)) → U27_gga(T281, T274, T276, lessA_in_g(T281))
U27_gga(T281, T274, T276, lessA_out_g(T281)) → deleteC_out_gga(s(T281), tree(s(T281), T274, void), tree(s(T281), T276, void))
U27_gga(T281, T274, T276, lessA_out_g(T281)) → U28_gga(T281, T274, T276, deleteC_in_gga(s(T281), T274, T276))
deleteC_in_gga(T292, tree(T292, T293, void), tree(T292, T293, T295)) → U29_gga(T292, T293, T295, pB_in_ga(T292, T295))
U29_gga(T292, T293, T295, pB_out_ga(T292, T295)) → deleteC_out_gga(T292, tree(T292, T293, void), tree(T292, T293, T295))
deleteC_in_gga(s(T305), tree(s(T305), T300, void), tree(s(T305), T300, T302)) → U30_gga(T305, T300, T302, lessA_in_g(T305))
U30_gga(T305, T300, T302, lessA_out_g(T305)) → deleteC_out_gga(s(T305), tree(s(T305), T300, void), tree(s(T305), T300, T302))
U30_gga(T305, T300, T302, lessA_out_g(T305)) → U31_gga(T305, T300, T302, deleteC_in_gga(s(T305), void, T302))
deleteC_in_gga(T313, tree(T313, T314, tree(T328, void, T329)), tree(T328, T314, T329)) → deleteC_out_gga(T313, tree(T313, T314, tree(T328, void, T329)), tree(T328, T314, T329))
deleteC_in_gga(T313, tree(T313, T314, tree(T354, T355, T356)), tree(T360, T314, tree(T354, T361, T359))) → U32_gga(T313, T314, T354, T355, T356, T360, T361, T359, delminE_in_gaa(T355, T360, T361))
U32_gga(T313, T314, T354, T355, T356, T360, T361, T359, delminE_out_gaa(T355, T360, T361)) → deleteC_out_gga(T313, tree(T313, T314, tree(T354, T355, T356)), tree(T360, T314, tree(T354, T361, T359)))
deleteC_in_gga(T382, tree(T382, T383, T384), tree(T382, T386, T384)) → U33_gga(T382, T383, T384, T386, lessA_in_g(T382))
U33_gga(T382, T383, T384, T386, lessA_out_g(T382)) → deleteC_out_gga(T382, tree(T382, T383, T384), tree(T382, T386, T384))
U33_gga(T382, T383, T384, T386, lessA_out_g(T382)) → U34_gga(T382, T383, T384, T386, deleteC_in_gga(T382, T383, T386))
deleteC_in_gga(T399, tree(T399, T400, T401), tree(T399, T400, T403)) → U35_gga(T399, T400, T401, T403, lessA_in_g(T399))
U35_gga(T399, T400, T401, T403, lessA_out_g(T399)) → deleteC_out_gga(T399, tree(T399, T400, T401), tree(T399, T400, T403))
U35_gga(T399, T400, T401, T403, lessA_out_g(T399)) → U36_gga(T399, T400, T401, T403, deleteC_in_gga(T399, T401, T403))
deleteC_in_gga(0, tree(s(T423), T415, T416), tree(s(T423), T418, T416)) → U37_gga(T423, T415, T416, T418, deleteC_in_gga(0, T415, T418))
deleteC_in_gga(s(T434), tree(s(T435), T415, T416), tree(s(T435), T418, T416)) → U38_gga(T434, T435, T415, T416, T418, lessH_in_gg(T434, T435))
lessH_in_gg(0, s(T444)) → lessH_out_gg(0, s(T444))
lessH_in_gg(s(0), s(s(T457))) → lessH_out_gg(s(0), s(s(T457)))
lessH_in_gg(s(s(0)), s(s(s(T470)))) → lessH_out_gg(s(s(0)), s(s(s(T470))))
lessH_in_gg(s(s(s(0))), s(s(s(s(T483))))) → lessH_out_gg(s(s(s(0))), s(s(s(s(T483)))))
lessH_in_gg(s(s(s(s(0)))), s(s(s(s(s(T496)))))) → lessH_out_gg(s(s(s(s(0)))), s(s(s(s(s(T496))))))
lessH_in_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T509))))))) → lessH_out_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T509)))))))
lessH_in_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T522)))))))) → lessH_out_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T522))))))))
lessH_in_gg(s(s(s(s(s(s(s(T527))))))), s(s(s(s(s(s(s(T528)))))))) → U10_gg(T527, T528, lessG_in_gg(T527, T528))
lessG_in_gg(0, s(T539)) → lessG_out_gg(0, s(T539))
lessG_in_gg(s(T544), s(T545)) → U9_gg(T544, T545, lessG_in_gg(T544, T545))
U9_gg(T544, T545, lessG_out_gg(T544, T545)) → lessG_out_gg(s(T544), s(T545))
U10_gg(T527, T528, lessG_out_gg(T527, T528)) → lessH_out_gg(s(s(s(s(s(s(s(T527))))))), s(s(s(s(s(s(s(T528))))))))
U38_gga(T434, T435, T415, T416, T418, lessH_out_gg(T434, T435)) → deleteC_out_gga(s(T434), tree(s(T435), T415, T416), tree(s(T435), T418, T416))
U38_gga(T434, T435, T415, T416, T418, lessH_out_gg(T434, T435)) → U39_gga(T434, T435, T415, T416, T418, deleteC_in_gga(s(T434), T415, T418))
deleteC_in_gga(T562, tree(T563, T564, T565), tree(T563, T564, T567)) → U40_gga(T562, T563, T564, T565, T567, lessG_in_gg(T563, T562))
U40_gga(T562, T563, T564, T565, T567, lessG_out_gg(T563, T562)) → deleteC_out_gga(T562, tree(T563, T564, T565), tree(T563, T564, T567))
U40_gga(T562, T563, T564, T565, T567, lessG_out_gg(T563, T562)) → U41_gga(T562, T563, T564, T565, T567, deleteC_in_gga(T562, T565, T567))
deleteC_in_gga(s(T591), tree(0, T583, T584), tree(0, T583, T586)) → U42_gga(T591, T583, T584, T586, deleteC_in_gga(s(T591), T584, T586))
deleteC_in_gga(s(T601), tree(s(T600), T583, T584), tree(s(T600), T583, T586)) → U43_gga(T601, T600, T583, T584, T586, lessG_in_gg(T600, T601))
U43_gga(T601, T600, T583, T584, T586, lessG_out_gg(T600, T601)) → deleteC_out_gga(s(T601), tree(s(T600), T583, T584), tree(s(T600), T583, T586))
U43_gga(T601, T600, T583, T584, T586, lessG_out_gg(T600, T601)) → U44_gga(T601, T600, T583, T584, T586, deleteC_in_gga(s(T601), T584, T586))
U44_gga(T601, T600, T583, T584, T586, deleteC_out_gga(s(T601), T584, T586)) → deleteC_out_gga(s(T601), tree(s(T600), T583, T584), tree(s(T600), T583, T586))
U42_gga(T591, T583, T584, T586, deleteC_out_gga(s(T591), T584, T586)) → deleteC_out_gga(s(T591), tree(0, T583, T584), tree(0, T583, T586))
U41_gga(T562, T563, T564, T565, T567, deleteC_out_gga(T562, T565, T567)) → deleteC_out_gga(T562, tree(T563, T564, T565), tree(T563, T564, T567))
U39_gga(T434, T435, T415, T416, T418, deleteC_out_gga(s(T434), T415, T418)) → deleteC_out_gga(s(T434), tree(s(T435), T415, T416), tree(s(T435), T418, T416))
U37_gga(T423, T415, T416, T418, deleteC_out_gga(0, T415, T418)) → deleteC_out_gga(0, tree(s(T423), T415, T416), tree(s(T423), T418, T416))
U36_gga(T399, T400, T401, T403, deleteC_out_gga(T399, T401, T403)) → deleteC_out_gga(T399, tree(T399, T400, T401), tree(T399, T400, T403))
U34_gga(T382, T383, T384, T386, deleteC_out_gga(T382, T383, T386)) → deleteC_out_gga(T382, tree(T382, T383, T384), tree(T382, T386, T384))
U31_gga(T305, T300, T302, deleteC_out_gga(s(T305), void, T302)) → deleteC_out_gga(s(T305), tree(s(T305), T300, void), tree(s(T305), T300, T302))
U28_gga(T281, T274, T276, deleteC_out_gga(s(T281), T274, T276)) → deleteC_out_gga(s(T281), tree(s(T281), T274, void), tree(s(T281), T276, void))
U25_gga(T252, T253, T255, deleteC_out_gga(T252, T253, T255)) → deleteC_out_gga(T252, tree(T252, T253, void), tree(T252, T255, void))
U23_gga(T221, T216, T218, deleteC_out_gga(s(T221), T216, T218)) → deleteC_out_gga(s(T221), tree(s(T221), void, T216), tree(s(T221), void, T218))
U20_gga(T199, T192, T194, deleteC_out_gga(s(T199), void, T194)) → deleteC_out_gga(s(T199), tree(s(T199), void, T192), tree(s(T199), T194, T192))
U8_gga(T180, T181, T183, deleteC_out_gga(T180, T181, T183)) → pF_out_gga(T180, T181, T183)
U18_gga(T180, T181, T183, pF_out_gga(T180, T181, T183)) → deleteC_out_gga(T180, tree(T180, void, T181), tree(T180, void, T183))
U5_ga(T50, T45, deleteC_out_gga(s(T50), void, T45)) → pD_out_ga(T50, T45)
U13_gga(T50, T45, pD_out_ga(T50, T45)) → deleteC_out_gga(s(T50), tree(s(T50), void, void), tree(s(T50), T45, void))
U3_ga(T26, T28, deleteC_out_gga(T26, void, T28)) → pB_out_ga(T26, T28)
U11_gga(T26, T28, pB_out_ga(T26, T28)) → deleteC_out_gga(T26, tree(T26, void, void), tree(T26, T28, void))

The argument filtering Pi contains the following mapping:
deleteC_in_gga(x1, x2, x3)  =  deleteC_in_gga(x1, x2)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
void  =  void
deleteC_out_gga(x1, x2, x3)  =  deleteC_out_gga
U11_gga(x1, x2, x3)  =  U11_gga(x3)
pB_in_ga(x1, x2)  =  pB_in_ga(x1)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
lessA_in_g(x1)  =  lessA_in_g(x1)
s(x1)  =  s(x1)
U1_g(x1, x2)  =  U1_g(x2)
lessA_out_g(x1)  =  lessA_out_g
pB_out_ga(x1, x2)  =  pB_out_ga
U3_ga(x1, x2, x3)  =  U3_ga(x3)
U12_gga(x1, x2, x3)  =  U12_gga(x3)
U13_gga(x1, x2, x3)  =  U13_gga(x3)
pD_in_ga(x1, x2)  =  pD_in_ga(x1)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
pD_out_ga(x1, x2)  =  pD_out_ga
U5_ga(x1, x2, x3)  =  U5_ga(x3)
U14_gga(x1, x2, x3)  =  U14_gga(x3)
U15_gga(x1, x2, x3)  =  U15_gga(x3)
U16_gga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U16_gga(x8)
delminE_in_gaa(x1, x2, x3)  =  delminE_in_gaa(x1)
delminE_out_gaa(x1, x2, x3)  =  delminE_out_gaa(x2)
U6_gaa(x1, x2, x3, x4, x5, x6, x7)  =  U6_gaa(x7)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x4)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x4)
pF_in_gga(x1, x2, x3)  =  pF_in_gga(x1, x2)
U7_gga(x1, x2, x3, x4)  =  U7_gga(x1, x2, x4)
pF_out_gga(x1, x2, x3)  =  pF_out_gga
U8_gga(x1, x2, x3, x4)  =  U8_gga(x4)
U19_gga(x1, x2, x3, x4)  =  U19_gga(x1, x4)
U20_gga(x1, x2, x3, x4)  =  U20_gga(x4)
U21_gga(x1, x2, x3, x4)  =  U21_gga(x4)
U22_gga(x1, x2, x3, x4)  =  U22_gga(x1, x2, x4)
U23_gga(x1, x2, x3, x4)  =  U23_gga(x4)
U24_gga(x1, x2, x3, x4)  =  U24_gga(x1, x2, x4)
U25_gga(x1, x2, x3, x4)  =  U25_gga(x4)
U26_gga(x1, x2, x3, x4)  =  U26_gga(x4)
U27_gga(x1, x2, x3, x4)  =  U27_gga(x1, x2, x4)
U28_gga(x1, x2, x3, x4)  =  U28_gga(x4)
U29_gga(x1, x2, x3, x4)  =  U29_gga(x4)
U30_gga(x1, x2, x3, x4)  =  U30_gga(x1, x4)
U31_gga(x1, x2, x3, x4)  =  U31_gga(x4)
U32_gga(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U32_gga(x9)
U33_gga(x1, x2, x3, x4, x5)  =  U33_gga(x1, x2, x5)
U34_gga(x1, x2, x3, x4, x5)  =  U34_gga(x5)
U35_gga(x1, x2, x3, x4, x5)  =  U35_gga(x1, x3, x5)
U36_gga(x1, x2, x3, x4, x5)  =  U36_gga(x5)
0  =  0
U37_gga(x1, x2, x3, x4, x5)  =  U37_gga(x5)
U38_gga(x1, x2, x3, x4, x5, x6)  =  U38_gga(x1, x3, x6)
lessH_in_gg(x1, x2)  =  lessH_in_gg(x1, x2)
lessH_out_gg(x1, x2)  =  lessH_out_gg
U10_gg(x1, x2, x3)  =  U10_gg(x3)
lessG_in_gg(x1, x2)  =  lessG_in_gg(x1, x2)
lessG_out_gg(x1, x2)  =  lessG_out_gg
U9_gg(x1, x2, x3)  =  U9_gg(x3)
U39_gga(x1, x2, x3, x4, x5, x6)  =  U39_gga(x6)
U40_gga(x1, x2, x3, x4, x5, x6)  =  U40_gga(x1, x4, x6)
U41_gga(x1, x2, x3, x4, x5, x6)  =  U41_gga(x6)
U42_gga(x1, x2, x3, x4, x5)  =  U42_gga(x5)
U43_gga(x1, x2, x3, x4, x5, x6)  =  U43_gga(x1, x4, x6)
U44_gga(x1, x2, x3, x4, x5, x6)  =  U44_gga(x6)

(5) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

DELETEC_IN_GGA(T26, tree(T26, void, void), tree(T26, T28, void)) → U11_GGA(T26, T28, pB_in_ga(T26, T28))
DELETEC_IN_GGA(T26, tree(T26, void, void), tree(T26, T28, void)) → PB_IN_GA(T26, T28)
PB_IN_GA(T26, T28) → U2_GA(T26, T28, lessA_in_g(T26))
PB_IN_GA(T26, T28) → LESSA_IN_G(T26)
LESSA_IN_G(s(T31)) → U1_G(T31, lessA_in_g(T31))
LESSA_IN_G(s(T31)) → LESSA_IN_G(T31)
U2_GA(T26, T28, lessA_out_g(T26)) → U3_GA(T26, T28, deleteC_in_gga(T26, void, T28))
U2_GA(T26, T28, lessA_out_g(T26)) → DELETEC_IN_GGA(T26, void, T28)
DELETEC_IN_GGA(T38, tree(T38, void, void), tree(T38, void, T40)) → U12_GGA(T38, T40, pB_in_ga(T38, T40))
DELETEC_IN_GGA(T38, tree(T38, void, void), tree(T38, void, T40)) → PB_IN_GA(T38, T40)
DELETEC_IN_GGA(s(T50), tree(s(T50), void, void), tree(s(T50), T45, void)) → U13_GGA(T50, T45, pD_in_ga(T50, T45))
DELETEC_IN_GGA(s(T50), tree(s(T50), void, void), tree(s(T50), T45, void)) → PD_IN_GA(T50, T45)
PD_IN_GA(T50, T45) → U4_GA(T50, T45, lessA_in_g(T50))
PD_IN_GA(T50, T45) → LESSA_IN_G(T50)
U4_GA(T50, T45, lessA_out_g(T50)) → U5_GA(T50, T45, deleteC_in_gga(s(T50), void, T45))
U4_GA(T50, T45, lessA_out_g(T50)) → DELETEC_IN_GGA(s(T50), void, T45)
DELETEC_IN_GGA(T57, tree(T57, void, void), tree(T57, void, T59)) → U14_GGA(T57, T59, pB_in_ga(T57, T59))
DELETEC_IN_GGA(s(T67), tree(s(T67), void, void), tree(s(T67), void, T64)) → U15_GGA(T67, T64, pD_in_ga(T67, T64))
DELETEC_IN_GGA(s(T67), tree(s(T67), void, void), tree(s(T67), void, T64)) → PD_IN_GA(T67, T64)
DELETEC_IN_GGA(T72, tree(T72, void, tree(T112, T113, T114)), tree(T118, void, tree(T112, T119, T117))) → U16_GGA(T72, T112, T113, T114, T118, T119, T117, delminE_in_gaa(T113, T118, T119))
DELETEC_IN_GGA(T72, tree(T72, void, tree(T112, T113, T114)), tree(T118, void, tree(T112, T119, T117))) → DELMINE_IN_GAA(T113, T118, T119)
DELMINE_IN_GAA(tree(T146, T147, T148), T152, tree(T146, T153, T151)) → U6_GAA(T146, T147, T148, T152, T153, T151, delminE_in_gaa(T147, T152, T153))
DELMINE_IN_GAA(tree(T146, T147, T148), T152, tree(T146, T153, T151)) → DELMINE_IN_GAA(T147, T152, T153)
DELETEC_IN_GGA(T170, tree(T170, void, T171), tree(T170, T173, T171)) → U17_GGA(T170, T171, T173, pB_in_ga(T170, T173))
DELETEC_IN_GGA(T170, tree(T170, void, T171), tree(T170, T173, T171)) → PB_IN_GA(T170, T173)
DELETEC_IN_GGA(T180, tree(T180, void, T181), tree(T180, void, T183)) → U18_GGA(T180, T181, T183, pF_in_gga(T180, T181, T183))
DELETEC_IN_GGA(T180, tree(T180, void, T181), tree(T180, void, T183)) → PF_IN_GGA(T180, T181, T183)
PF_IN_GGA(T180, T181, T183) → U7_GGA(T180, T181, T183, lessA_in_g(T180))
PF_IN_GGA(T180, T181, T183) → LESSA_IN_G(T180)
U7_GGA(T180, T181, T183, lessA_out_g(T180)) → U8_GGA(T180, T181, T183, deleteC_in_gga(T180, T181, T183))
U7_GGA(T180, T181, T183, lessA_out_g(T180)) → DELETEC_IN_GGA(T180, T181, T183)
DELETEC_IN_GGA(s(T199), tree(s(T199), void, T192), tree(s(T199), T194, T192)) → U19_GGA(T199, T192, T194, lessA_in_g(T199))
DELETEC_IN_GGA(s(T199), tree(s(T199), void, T192), tree(s(T199), T194, T192)) → LESSA_IN_G(T199)
U19_GGA(T199, T192, T194, lessA_out_g(T199)) → U20_GGA(T199, T192, T194, deleteC_in_gga(s(T199), void, T194))
U19_GGA(T199, T192, T194, lessA_out_g(T199)) → DELETEC_IN_GGA(s(T199), void, T194)
DELETEC_IN_GGA(T208, tree(T208, void, T209), tree(T208, void, T211)) → U21_GGA(T208, T209, T211, pF_in_gga(T208, T209, T211))
DELETEC_IN_GGA(s(T221), tree(s(T221), void, T216), tree(s(T221), void, T218)) → U22_GGA(T221, T216, T218, lessA_in_g(T221))
DELETEC_IN_GGA(s(T221), tree(s(T221), void, T216), tree(s(T221), void, T218)) → LESSA_IN_G(T221)
U22_GGA(T221, T216, T218, lessA_out_g(T221)) → U23_GGA(T221, T216, T218, deleteC_in_gga(s(T221), T216, T218))
U22_GGA(T221, T216, T218, lessA_out_g(T221)) → DELETEC_IN_GGA(s(T221), T216, T218)
DELETEC_IN_GGA(T252, tree(T252, T253, void), tree(T252, T255, void)) → U24_GGA(T252, T253, T255, lessA_in_g(T252))
DELETEC_IN_GGA(T252, tree(T252, T253, void), tree(T252, T255, void)) → LESSA_IN_G(T252)
U24_GGA(T252, T253, T255, lessA_out_g(T252)) → U25_GGA(T252, T253, T255, deleteC_in_gga(T252, T253, T255))
U24_GGA(T252, T253, T255, lessA_out_g(T252)) → DELETEC_IN_GGA(T252, T253, T255)
DELETEC_IN_GGA(T266, tree(T266, T267, void), tree(T266, T267, T269)) → U26_GGA(T266, T267, T269, pB_in_ga(T266, T269))
DELETEC_IN_GGA(T266, tree(T266, T267, void), tree(T266, T267, T269)) → PB_IN_GA(T266, T269)
DELETEC_IN_GGA(s(T281), tree(s(T281), T274, void), tree(s(T281), T276, void)) → U27_GGA(T281, T274, T276, lessA_in_g(T281))
DELETEC_IN_GGA(s(T281), tree(s(T281), T274, void), tree(s(T281), T276, void)) → LESSA_IN_G(T281)
U27_GGA(T281, T274, T276, lessA_out_g(T281)) → U28_GGA(T281, T274, T276, deleteC_in_gga(s(T281), T274, T276))
U27_GGA(T281, T274, T276, lessA_out_g(T281)) → DELETEC_IN_GGA(s(T281), T274, T276)
DELETEC_IN_GGA(T292, tree(T292, T293, void), tree(T292, T293, T295)) → U29_GGA(T292, T293, T295, pB_in_ga(T292, T295))
DELETEC_IN_GGA(s(T305), tree(s(T305), T300, void), tree(s(T305), T300, T302)) → U30_GGA(T305, T300, T302, lessA_in_g(T305))
DELETEC_IN_GGA(s(T305), tree(s(T305), T300, void), tree(s(T305), T300, T302)) → LESSA_IN_G(T305)
U30_GGA(T305, T300, T302, lessA_out_g(T305)) → U31_GGA(T305, T300, T302, deleteC_in_gga(s(T305), void, T302))
U30_GGA(T305, T300, T302, lessA_out_g(T305)) → DELETEC_IN_GGA(s(T305), void, T302)
DELETEC_IN_GGA(T313, tree(T313, T314, tree(T354, T355, T356)), tree(T360, T314, tree(T354, T361, T359))) → U32_GGA(T313, T314, T354, T355, T356, T360, T361, T359, delminE_in_gaa(T355, T360, T361))
DELETEC_IN_GGA(T313, tree(T313, T314, tree(T354, T355, T356)), tree(T360, T314, tree(T354, T361, T359))) → DELMINE_IN_GAA(T355, T360, T361)
DELETEC_IN_GGA(T382, tree(T382, T383, T384), tree(T382, T386, T384)) → U33_GGA(T382, T383, T384, T386, lessA_in_g(T382))
DELETEC_IN_GGA(T382, tree(T382, T383, T384), tree(T382, T386, T384)) → LESSA_IN_G(T382)
U33_GGA(T382, T383, T384, T386, lessA_out_g(T382)) → U34_GGA(T382, T383, T384, T386, deleteC_in_gga(T382, T383, T386))
U33_GGA(T382, T383, T384, T386, lessA_out_g(T382)) → DELETEC_IN_GGA(T382, T383, T386)
DELETEC_IN_GGA(T399, tree(T399, T400, T401), tree(T399, T400, T403)) → U35_GGA(T399, T400, T401, T403, lessA_in_g(T399))
DELETEC_IN_GGA(T399, tree(T399, T400, T401), tree(T399, T400, T403)) → LESSA_IN_G(T399)
U35_GGA(T399, T400, T401, T403, lessA_out_g(T399)) → U36_GGA(T399, T400, T401, T403, deleteC_in_gga(T399, T401, T403))
U35_GGA(T399, T400, T401, T403, lessA_out_g(T399)) → DELETEC_IN_GGA(T399, T401, T403)
DELETEC_IN_GGA(0, tree(s(T423), T415, T416), tree(s(T423), T418, T416)) → U37_GGA(T423, T415, T416, T418, deleteC_in_gga(0, T415, T418))
DELETEC_IN_GGA(0, tree(s(T423), T415, T416), tree(s(T423), T418, T416)) → DELETEC_IN_GGA(0, T415, T418)
DELETEC_IN_GGA(s(T434), tree(s(T435), T415, T416), tree(s(T435), T418, T416)) → U38_GGA(T434, T435, T415, T416, T418, lessH_in_gg(T434, T435))
DELETEC_IN_GGA(s(T434), tree(s(T435), T415, T416), tree(s(T435), T418, T416)) → LESSH_IN_GG(T434, T435)
LESSH_IN_GG(s(s(s(s(s(s(s(T527))))))), s(s(s(s(s(s(s(T528)))))))) → U10_GG(T527, T528, lessG_in_gg(T527, T528))
LESSH_IN_GG(s(s(s(s(s(s(s(T527))))))), s(s(s(s(s(s(s(T528)))))))) → LESSG_IN_GG(T527, T528)
LESSG_IN_GG(s(T544), s(T545)) → U9_GG(T544, T545, lessG_in_gg(T544, T545))
LESSG_IN_GG(s(T544), s(T545)) → LESSG_IN_GG(T544, T545)
U38_GGA(T434, T435, T415, T416, T418, lessH_out_gg(T434, T435)) → U39_GGA(T434, T435, T415, T416, T418, deleteC_in_gga(s(T434), T415, T418))
U38_GGA(T434, T435, T415, T416, T418, lessH_out_gg(T434, T435)) → DELETEC_IN_GGA(s(T434), T415, T418)
DELETEC_IN_GGA(T562, tree(T563, T564, T565), tree(T563, T564, T567)) → U40_GGA(T562, T563, T564, T565, T567, lessG_in_gg(T563, T562))
DELETEC_IN_GGA(T562, tree(T563, T564, T565), tree(T563, T564, T567)) → LESSG_IN_GG(T563, T562)
U40_GGA(T562, T563, T564, T565, T567, lessG_out_gg(T563, T562)) → U41_GGA(T562, T563, T564, T565, T567, deleteC_in_gga(T562, T565, T567))
U40_GGA(T562, T563, T564, T565, T567, lessG_out_gg(T563, T562)) → DELETEC_IN_GGA(T562, T565, T567)
DELETEC_IN_GGA(s(T591), tree(0, T583, T584), tree(0, T583, T586)) → U42_GGA(T591, T583, T584, T586, deleteC_in_gga(s(T591), T584, T586))
DELETEC_IN_GGA(s(T591), tree(0, T583, T584), tree(0, T583, T586)) → DELETEC_IN_GGA(s(T591), T584, T586)
DELETEC_IN_GGA(s(T601), tree(s(T600), T583, T584), tree(s(T600), T583, T586)) → U43_GGA(T601, T600, T583, T584, T586, lessG_in_gg(T600, T601))
DELETEC_IN_GGA(s(T601), tree(s(T600), T583, T584), tree(s(T600), T583, T586)) → LESSG_IN_GG(T600, T601)
U43_GGA(T601, T600, T583, T584, T586, lessG_out_gg(T600, T601)) → U44_GGA(T601, T600, T583, T584, T586, deleteC_in_gga(s(T601), T584, T586))
U43_GGA(T601, T600, T583, T584, T586, lessG_out_gg(T600, T601)) → DELETEC_IN_GGA(s(T601), T584, T586)

The TRS R consists of the following rules:

deleteC_in_gga(T6, tree(T6, void, T7), T7) → deleteC_out_gga(T6, tree(T6, void, T7), T7)
deleteC_in_gga(T9, tree(T9, void, void), void) → deleteC_out_gga(T9, tree(T9, void, void), void)
deleteC_in_gga(T26, tree(T26, void, void), tree(T26, T28, void)) → U11_gga(T26, T28, pB_in_ga(T26, T28))
pB_in_ga(T26, T28) → U2_ga(T26, T28, lessA_in_g(T26))
lessA_in_g(s(T31)) → U1_g(T31, lessA_in_g(T31))
U1_g(T31, lessA_out_g(T31)) → lessA_out_g(s(T31))
U2_ga(T26, T28, lessA_out_g(T26)) → pB_out_ga(T26, T28)
U2_ga(T26, T28, lessA_out_g(T26)) → U3_ga(T26, T28, deleteC_in_gga(T26, void, T28))
deleteC_in_gga(T38, tree(T38, void, void), tree(T38, void, T40)) → U12_gga(T38, T40, pB_in_ga(T38, T40))
U12_gga(T38, T40, pB_out_ga(T38, T40)) → deleteC_out_gga(T38, tree(T38, void, void), tree(T38, void, T40))
deleteC_in_gga(s(T50), tree(s(T50), void, void), tree(s(T50), T45, void)) → U13_gga(T50, T45, pD_in_ga(T50, T45))
pD_in_ga(T50, T45) → U4_ga(T50, T45, lessA_in_g(T50))
U4_ga(T50, T45, lessA_out_g(T50)) → pD_out_ga(T50, T45)
U4_ga(T50, T45, lessA_out_g(T50)) → U5_ga(T50, T45, deleteC_in_gga(s(T50), void, T45))
deleteC_in_gga(T57, tree(T57, void, void), tree(T57, void, T59)) → U14_gga(T57, T59, pB_in_ga(T57, T59))
U14_gga(T57, T59, pB_out_ga(T57, T59)) → deleteC_out_gga(T57, tree(T57, void, void), tree(T57, void, T59))
deleteC_in_gga(s(T67), tree(s(T67), void, void), tree(s(T67), void, T64)) → U15_gga(T67, T64, pD_in_ga(T67, T64))
U15_gga(T67, T64, pD_out_ga(T67, T64)) → deleteC_out_gga(s(T67), tree(s(T67), void, void), tree(s(T67), void, T64))
deleteC_in_gga(T72, tree(T72, void, tree(T86, void, T87)), tree(T86, void, T87)) → deleteC_out_gga(T72, tree(T72, void, tree(T86, void, T87)), tree(T86, void, T87))
deleteC_in_gga(T72, tree(T72, void, tree(T112, T113, T114)), tree(T118, void, tree(T112, T119, T117))) → U16_gga(T72, T112, T113, T114, T118, T119, T117, delminE_in_gaa(T113, T118, T119))
delminE_in_gaa(tree(T132, void, T133), T132, T133) → delminE_out_gaa(tree(T132, void, T133), T132, T133)
delminE_in_gaa(tree(T146, T147, T148), T152, tree(T146, T153, T151)) → U6_gaa(T146, T147, T148, T152, T153, T151, delminE_in_gaa(T147, T152, T153))
U6_gaa(T146, T147, T148, T152, T153, T151, delminE_out_gaa(T147, T152, T153)) → delminE_out_gaa(tree(T146, T147, T148), T152, tree(T146, T153, T151))
U16_gga(T72, T112, T113, T114, T118, T119, T117, delminE_out_gaa(T113, T118, T119)) → deleteC_out_gga(T72, tree(T72, void, tree(T112, T113, T114)), tree(T118, void, tree(T112, T119, T117)))
deleteC_in_gga(T170, tree(T170, void, T171), tree(T170, T173, T171)) → U17_gga(T170, T171, T173, pB_in_ga(T170, T173))
U17_gga(T170, T171, T173, pB_out_ga(T170, T173)) → deleteC_out_gga(T170, tree(T170, void, T171), tree(T170, T173, T171))
deleteC_in_gga(T180, tree(T180, void, T181), tree(T180, void, T183)) → U18_gga(T180, T181, T183, pF_in_gga(T180, T181, T183))
pF_in_gga(T180, T181, T183) → U7_gga(T180, T181, T183, lessA_in_g(T180))
U7_gga(T180, T181, T183, lessA_out_g(T180)) → pF_out_gga(T180, T181, T183)
U7_gga(T180, T181, T183, lessA_out_g(T180)) → U8_gga(T180, T181, T183, deleteC_in_gga(T180, T181, T183))
deleteC_in_gga(s(T199), tree(s(T199), void, T192), tree(s(T199), T194, T192)) → U19_gga(T199, T192, T194, lessA_in_g(T199))
U19_gga(T199, T192, T194, lessA_out_g(T199)) → deleteC_out_gga(s(T199), tree(s(T199), void, T192), tree(s(T199), T194, T192))
U19_gga(T199, T192, T194, lessA_out_g(T199)) → U20_gga(T199, T192, T194, deleteC_in_gga(s(T199), void, T194))
deleteC_in_gga(T208, tree(T208, void, T209), tree(T208, void, T211)) → U21_gga(T208, T209, T211, pF_in_gga(T208, T209, T211))
U21_gga(T208, T209, T211, pF_out_gga(T208, T209, T211)) → deleteC_out_gga(T208, tree(T208, void, T209), tree(T208, void, T211))
deleteC_in_gga(s(T221), tree(s(T221), void, T216), tree(s(T221), void, T218)) → U22_gga(T221, T216, T218, lessA_in_g(T221))
U22_gga(T221, T216, T218, lessA_out_g(T221)) → deleteC_out_gga(s(T221), tree(s(T221), void, T216), tree(s(T221), void, T218))
U22_gga(T221, T216, T218, lessA_out_g(T221)) → U23_gga(T221, T216, T218, deleteC_in_gga(s(T221), T216, T218))
deleteC_in_gga(T228, tree(T228, T229, void), T229) → deleteC_out_gga(T228, tree(T228, T229, void), T229)
deleteC_in_gga(T252, tree(T252, T253, void), tree(T252, T255, void)) → U24_gga(T252, T253, T255, lessA_in_g(T252))
U24_gga(T252, T253, T255, lessA_out_g(T252)) → deleteC_out_gga(T252, tree(T252, T253, void), tree(T252, T255, void))
U24_gga(T252, T253, T255, lessA_out_g(T252)) → U25_gga(T252, T253, T255, deleteC_in_gga(T252, T253, T255))
deleteC_in_gga(T266, tree(T266, T267, void), tree(T266, T267, T269)) → U26_gga(T266, T267, T269, pB_in_ga(T266, T269))
U26_gga(T266, T267, T269, pB_out_ga(T266, T269)) → deleteC_out_gga(T266, tree(T266, T267, void), tree(T266, T267, T269))
deleteC_in_gga(s(T281), tree(s(T281), T274, void), tree(s(T281), T276, void)) → U27_gga(T281, T274, T276, lessA_in_g(T281))
U27_gga(T281, T274, T276, lessA_out_g(T281)) → deleteC_out_gga(s(T281), tree(s(T281), T274, void), tree(s(T281), T276, void))
U27_gga(T281, T274, T276, lessA_out_g(T281)) → U28_gga(T281, T274, T276, deleteC_in_gga(s(T281), T274, T276))
deleteC_in_gga(T292, tree(T292, T293, void), tree(T292, T293, T295)) → U29_gga(T292, T293, T295, pB_in_ga(T292, T295))
U29_gga(T292, T293, T295, pB_out_ga(T292, T295)) → deleteC_out_gga(T292, tree(T292, T293, void), tree(T292, T293, T295))
deleteC_in_gga(s(T305), tree(s(T305), T300, void), tree(s(T305), T300, T302)) → U30_gga(T305, T300, T302, lessA_in_g(T305))
U30_gga(T305, T300, T302, lessA_out_g(T305)) → deleteC_out_gga(s(T305), tree(s(T305), T300, void), tree(s(T305), T300, T302))
U30_gga(T305, T300, T302, lessA_out_g(T305)) → U31_gga(T305, T300, T302, deleteC_in_gga(s(T305), void, T302))
deleteC_in_gga(T313, tree(T313, T314, tree(T328, void, T329)), tree(T328, T314, T329)) → deleteC_out_gga(T313, tree(T313, T314, tree(T328, void, T329)), tree(T328, T314, T329))
deleteC_in_gga(T313, tree(T313, T314, tree(T354, T355, T356)), tree(T360, T314, tree(T354, T361, T359))) → U32_gga(T313, T314, T354, T355, T356, T360, T361, T359, delminE_in_gaa(T355, T360, T361))
U32_gga(T313, T314, T354, T355, T356, T360, T361, T359, delminE_out_gaa(T355, T360, T361)) → deleteC_out_gga(T313, tree(T313, T314, tree(T354, T355, T356)), tree(T360, T314, tree(T354, T361, T359)))
deleteC_in_gga(T382, tree(T382, T383, T384), tree(T382, T386, T384)) → U33_gga(T382, T383, T384, T386, lessA_in_g(T382))
U33_gga(T382, T383, T384, T386, lessA_out_g(T382)) → deleteC_out_gga(T382, tree(T382, T383, T384), tree(T382, T386, T384))
U33_gga(T382, T383, T384, T386, lessA_out_g(T382)) → U34_gga(T382, T383, T384, T386, deleteC_in_gga(T382, T383, T386))
deleteC_in_gga(T399, tree(T399, T400, T401), tree(T399, T400, T403)) → U35_gga(T399, T400, T401, T403, lessA_in_g(T399))
U35_gga(T399, T400, T401, T403, lessA_out_g(T399)) → deleteC_out_gga(T399, tree(T399, T400, T401), tree(T399, T400, T403))
U35_gga(T399, T400, T401, T403, lessA_out_g(T399)) → U36_gga(T399, T400, T401, T403, deleteC_in_gga(T399, T401, T403))
deleteC_in_gga(0, tree(s(T423), T415, T416), tree(s(T423), T418, T416)) → U37_gga(T423, T415, T416, T418, deleteC_in_gga(0, T415, T418))
deleteC_in_gga(s(T434), tree(s(T435), T415, T416), tree(s(T435), T418, T416)) → U38_gga(T434, T435, T415, T416, T418, lessH_in_gg(T434, T435))
lessH_in_gg(0, s(T444)) → lessH_out_gg(0, s(T444))
lessH_in_gg(s(0), s(s(T457))) → lessH_out_gg(s(0), s(s(T457)))
lessH_in_gg(s(s(0)), s(s(s(T470)))) → lessH_out_gg(s(s(0)), s(s(s(T470))))
lessH_in_gg(s(s(s(0))), s(s(s(s(T483))))) → lessH_out_gg(s(s(s(0))), s(s(s(s(T483)))))
lessH_in_gg(s(s(s(s(0)))), s(s(s(s(s(T496)))))) → lessH_out_gg(s(s(s(s(0)))), s(s(s(s(s(T496))))))
lessH_in_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T509))))))) → lessH_out_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T509)))))))
lessH_in_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T522)))))))) → lessH_out_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T522))))))))
lessH_in_gg(s(s(s(s(s(s(s(T527))))))), s(s(s(s(s(s(s(T528)))))))) → U10_gg(T527, T528, lessG_in_gg(T527, T528))
lessG_in_gg(0, s(T539)) → lessG_out_gg(0, s(T539))
lessG_in_gg(s(T544), s(T545)) → U9_gg(T544, T545, lessG_in_gg(T544, T545))
U9_gg(T544, T545, lessG_out_gg(T544, T545)) → lessG_out_gg(s(T544), s(T545))
U10_gg(T527, T528, lessG_out_gg(T527, T528)) → lessH_out_gg(s(s(s(s(s(s(s(T527))))))), s(s(s(s(s(s(s(T528))))))))
U38_gga(T434, T435, T415, T416, T418, lessH_out_gg(T434, T435)) → deleteC_out_gga(s(T434), tree(s(T435), T415, T416), tree(s(T435), T418, T416))
U38_gga(T434, T435, T415, T416, T418, lessH_out_gg(T434, T435)) → U39_gga(T434, T435, T415, T416, T418, deleteC_in_gga(s(T434), T415, T418))
deleteC_in_gga(T562, tree(T563, T564, T565), tree(T563, T564, T567)) → U40_gga(T562, T563, T564, T565, T567, lessG_in_gg(T563, T562))
U40_gga(T562, T563, T564, T565, T567, lessG_out_gg(T563, T562)) → deleteC_out_gga(T562, tree(T563, T564, T565), tree(T563, T564, T567))
U40_gga(T562, T563, T564, T565, T567, lessG_out_gg(T563, T562)) → U41_gga(T562, T563, T564, T565, T567, deleteC_in_gga(T562, T565, T567))
deleteC_in_gga(s(T591), tree(0, T583, T584), tree(0, T583, T586)) → U42_gga(T591, T583, T584, T586, deleteC_in_gga(s(T591), T584, T586))
deleteC_in_gga(s(T601), tree(s(T600), T583, T584), tree(s(T600), T583, T586)) → U43_gga(T601, T600, T583, T584, T586, lessG_in_gg(T600, T601))
U43_gga(T601, T600, T583, T584, T586, lessG_out_gg(T600, T601)) → deleteC_out_gga(s(T601), tree(s(T600), T583, T584), tree(s(T600), T583, T586))
U43_gga(T601, T600, T583, T584, T586, lessG_out_gg(T600, T601)) → U44_gga(T601, T600, T583, T584, T586, deleteC_in_gga(s(T601), T584, T586))
U44_gga(T601, T600, T583, T584, T586, deleteC_out_gga(s(T601), T584, T586)) → deleteC_out_gga(s(T601), tree(s(T600), T583, T584), tree(s(T600), T583, T586))
U42_gga(T591, T583, T584, T586, deleteC_out_gga(s(T591), T584, T586)) → deleteC_out_gga(s(T591), tree(0, T583, T584), tree(0, T583, T586))
U41_gga(T562, T563, T564, T565, T567, deleteC_out_gga(T562, T565, T567)) → deleteC_out_gga(T562, tree(T563, T564, T565), tree(T563, T564, T567))
U39_gga(T434, T435, T415, T416, T418, deleteC_out_gga(s(T434), T415, T418)) → deleteC_out_gga(s(T434), tree(s(T435), T415, T416), tree(s(T435), T418, T416))
U37_gga(T423, T415, T416, T418, deleteC_out_gga(0, T415, T418)) → deleteC_out_gga(0, tree(s(T423), T415, T416), tree(s(T423), T418, T416))
U36_gga(T399, T400, T401, T403, deleteC_out_gga(T399, T401, T403)) → deleteC_out_gga(T399, tree(T399, T400, T401), tree(T399, T400, T403))
U34_gga(T382, T383, T384, T386, deleteC_out_gga(T382, T383, T386)) → deleteC_out_gga(T382, tree(T382, T383, T384), tree(T382, T386, T384))
U31_gga(T305, T300, T302, deleteC_out_gga(s(T305), void, T302)) → deleteC_out_gga(s(T305), tree(s(T305), T300, void), tree(s(T305), T300, T302))
U28_gga(T281, T274, T276, deleteC_out_gga(s(T281), T274, T276)) → deleteC_out_gga(s(T281), tree(s(T281), T274, void), tree(s(T281), T276, void))
U25_gga(T252, T253, T255, deleteC_out_gga(T252, T253, T255)) → deleteC_out_gga(T252, tree(T252, T253, void), tree(T252, T255, void))
U23_gga(T221, T216, T218, deleteC_out_gga(s(T221), T216, T218)) → deleteC_out_gga(s(T221), tree(s(T221), void, T216), tree(s(T221), void, T218))
U20_gga(T199, T192, T194, deleteC_out_gga(s(T199), void, T194)) → deleteC_out_gga(s(T199), tree(s(T199), void, T192), tree(s(T199), T194, T192))
U8_gga(T180, T181, T183, deleteC_out_gga(T180, T181, T183)) → pF_out_gga(T180, T181, T183)
U18_gga(T180, T181, T183, pF_out_gga(T180, T181, T183)) → deleteC_out_gga(T180, tree(T180, void, T181), tree(T180, void, T183))
U5_ga(T50, T45, deleteC_out_gga(s(T50), void, T45)) → pD_out_ga(T50, T45)
U13_gga(T50, T45, pD_out_ga(T50, T45)) → deleteC_out_gga(s(T50), tree(s(T50), void, void), tree(s(T50), T45, void))
U3_ga(T26, T28, deleteC_out_gga(T26, void, T28)) → pB_out_ga(T26, T28)
U11_gga(T26, T28, pB_out_ga(T26, T28)) → deleteC_out_gga(T26, tree(T26, void, void), tree(T26, T28, void))

The argument filtering Pi contains the following mapping:
deleteC_in_gga(x1, x2, x3)  =  deleteC_in_gga(x1, x2)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
void  =  void
deleteC_out_gga(x1, x2, x3)  =  deleteC_out_gga
U11_gga(x1, x2, x3)  =  U11_gga(x3)
pB_in_ga(x1, x2)  =  pB_in_ga(x1)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
lessA_in_g(x1)  =  lessA_in_g(x1)
s(x1)  =  s(x1)
U1_g(x1, x2)  =  U1_g(x2)
lessA_out_g(x1)  =  lessA_out_g
pB_out_ga(x1, x2)  =  pB_out_ga
U3_ga(x1, x2, x3)  =  U3_ga(x3)
U12_gga(x1, x2, x3)  =  U12_gga(x3)
U13_gga(x1, x2, x3)  =  U13_gga(x3)
pD_in_ga(x1, x2)  =  pD_in_ga(x1)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
pD_out_ga(x1, x2)  =  pD_out_ga
U5_ga(x1, x2, x3)  =  U5_ga(x3)
U14_gga(x1, x2, x3)  =  U14_gga(x3)
U15_gga(x1, x2, x3)  =  U15_gga(x3)
U16_gga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U16_gga(x8)
delminE_in_gaa(x1, x2, x3)  =  delminE_in_gaa(x1)
delminE_out_gaa(x1, x2, x3)  =  delminE_out_gaa(x2)
U6_gaa(x1, x2, x3, x4, x5, x6, x7)  =  U6_gaa(x7)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x4)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x4)
pF_in_gga(x1, x2, x3)  =  pF_in_gga(x1, x2)
U7_gga(x1, x2, x3, x4)  =  U7_gga(x1, x2, x4)
pF_out_gga(x1, x2, x3)  =  pF_out_gga
U8_gga(x1, x2, x3, x4)  =  U8_gga(x4)
U19_gga(x1, x2, x3, x4)  =  U19_gga(x1, x4)
U20_gga(x1, x2, x3, x4)  =  U20_gga(x4)
U21_gga(x1, x2, x3, x4)  =  U21_gga(x4)
U22_gga(x1, x2, x3, x4)  =  U22_gga(x1, x2, x4)
U23_gga(x1, x2, x3, x4)  =  U23_gga(x4)
U24_gga(x1, x2, x3, x4)  =  U24_gga(x1, x2, x4)
U25_gga(x1, x2, x3, x4)  =  U25_gga(x4)
U26_gga(x1, x2, x3, x4)  =  U26_gga(x4)
U27_gga(x1, x2, x3, x4)  =  U27_gga(x1, x2, x4)
U28_gga(x1, x2, x3, x4)  =  U28_gga(x4)
U29_gga(x1, x2, x3, x4)  =  U29_gga(x4)
U30_gga(x1, x2, x3, x4)  =  U30_gga(x1, x4)
U31_gga(x1, x2, x3, x4)  =  U31_gga(x4)
U32_gga(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U32_gga(x9)
U33_gga(x1, x2, x3, x4, x5)  =  U33_gga(x1, x2, x5)
U34_gga(x1, x2, x3, x4, x5)  =  U34_gga(x5)
U35_gga(x1, x2, x3, x4, x5)  =  U35_gga(x1, x3, x5)
U36_gga(x1, x2, x3, x4, x5)  =  U36_gga(x5)
0  =  0
U37_gga(x1, x2, x3, x4, x5)  =  U37_gga(x5)
U38_gga(x1, x2, x3, x4, x5, x6)  =  U38_gga(x1, x3, x6)
lessH_in_gg(x1, x2)  =  lessH_in_gg(x1, x2)
lessH_out_gg(x1, x2)  =  lessH_out_gg
U10_gg(x1, x2, x3)  =  U10_gg(x3)
lessG_in_gg(x1, x2)  =  lessG_in_gg(x1, x2)
lessG_out_gg(x1, x2)  =  lessG_out_gg
U9_gg(x1, x2, x3)  =  U9_gg(x3)
U39_gga(x1, x2, x3, x4, x5, x6)  =  U39_gga(x6)
U40_gga(x1, x2, x3, x4, x5, x6)  =  U40_gga(x1, x4, x6)
U41_gga(x1, x2, x3, x4, x5, x6)  =  U41_gga(x6)
U42_gga(x1, x2, x3, x4, x5)  =  U42_gga(x5)
U43_gga(x1, x2, x3, x4, x5, x6)  =  U43_gga(x1, x4, x6)
U44_gga(x1, x2, x3, x4, x5, x6)  =  U44_gga(x6)
DELETEC_IN_GGA(x1, x2, x3)  =  DELETEC_IN_GGA(x1, x2)
U11_GGA(x1, x2, x3)  =  U11_GGA(x3)
PB_IN_GA(x1, x2)  =  PB_IN_GA(x1)
U2_GA(x1, x2, x3)  =  U2_GA(x1, x3)
LESSA_IN_G(x1)  =  LESSA_IN_G(x1)
U1_G(x1, x2)  =  U1_G(x2)
U3_GA(x1, x2, x3)  =  U3_GA(x3)
U12_GGA(x1, x2, x3)  =  U12_GGA(x3)
U13_GGA(x1, x2, x3)  =  U13_GGA(x3)
PD_IN_GA(x1, x2)  =  PD_IN_GA(x1)
U4_GA(x1, x2, x3)  =  U4_GA(x1, x3)
U5_GA(x1, x2, x3)  =  U5_GA(x3)
U14_GGA(x1, x2, x3)  =  U14_GGA(x3)
U15_GGA(x1, x2, x3)  =  U15_GGA(x3)
U16_GGA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U16_GGA(x8)
DELMINE_IN_GAA(x1, x2, x3)  =  DELMINE_IN_GAA(x1)
U6_GAA(x1, x2, x3, x4, x5, x6, x7)  =  U6_GAA(x7)
U17_GGA(x1, x2, x3, x4)  =  U17_GGA(x4)
U18_GGA(x1, x2, x3, x4)  =  U18_GGA(x4)
PF_IN_GGA(x1, x2, x3)  =  PF_IN_GGA(x1, x2)
U7_GGA(x1, x2, x3, x4)  =  U7_GGA(x1, x2, x4)
U8_GGA(x1, x2, x3, x4)  =  U8_GGA(x4)
U19_GGA(x1, x2, x3, x4)  =  U19_GGA(x1, x4)
U20_GGA(x1, x2, x3, x4)  =  U20_GGA(x4)
U21_GGA(x1, x2, x3, x4)  =  U21_GGA(x4)
U22_GGA(x1, x2, x3, x4)  =  U22_GGA(x1, x2, x4)
U23_GGA(x1, x2, x3, x4)  =  U23_GGA(x4)
U24_GGA(x1, x2, x3, x4)  =  U24_GGA(x1, x2, x4)
U25_GGA(x1, x2, x3, x4)  =  U25_GGA(x4)
U26_GGA(x1, x2, x3, x4)  =  U26_GGA(x4)
U27_GGA(x1, x2, x3, x4)  =  U27_GGA(x1, x2, x4)
U28_GGA(x1, x2, x3, x4)  =  U28_GGA(x4)
U29_GGA(x1, x2, x3, x4)  =  U29_GGA(x4)
U30_GGA(x1, x2, x3, x4)  =  U30_GGA(x1, x4)
U31_GGA(x1, x2, x3, x4)  =  U31_GGA(x4)
U32_GGA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U32_GGA(x9)
U33_GGA(x1, x2, x3, x4, x5)  =  U33_GGA(x1, x2, x5)
U34_GGA(x1, x2, x3, x4, x5)  =  U34_GGA(x5)
U35_GGA(x1, x2, x3, x4, x5)  =  U35_GGA(x1, x3, x5)
U36_GGA(x1, x2, x3, x4, x5)  =  U36_GGA(x5)
U37_GGA(x1, x2, x3, x4, x5)  =  U37_GGA(x5)
U38_GGA(x1, x2, x3, x4, x5, x6)  =  U38_GGA(x1, x3, x6)
LESSH_IN_GG(x1, x2)  =  LESSH_IN_GG(x1, x2)
U10_GG(x1, x2, x3)  =  U10_GG(x3)
LESSG_IN_GG(x1, x2)  =  LESSG_IN_GG(x1, x2)
U9_GG(x1, x2, x3)  =  U9_GG(x3)
U39_GGA(x1, x2, x3, x4, x5, x6)  =  U39_GGA(x6)
U40_GGA(x1, x2, x3, x4, x5, x6)  =  U40_GGA(x1, x4, x6)
U41_GGA(x1, x2, x3, x4, x5, x6)  =  U41_GGA(x6)
U42_GGA(x1, x2, x3, x4, x5)  =  U42_GGA(x5)
U43_GGA(x1, x2, x3, x4, x5, x6)  =  U43_GGA(x1, x4, x6)
U44_GGA(x1, x2, x3, x4, x5, x6)  =  U44_GGA(x6)

We have to consider all (P,R,Pi)-chains

(6) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

DELETEC_IN_GGA(T26, tree(T26, void, void), tree(T26, T28, void)) → U11_GGA(T26, T28, pB_in_ga(T26, T28))
DELETEC_IN_GGA(T26, tree(T26, void, void), tree(T26, T28, void)) → PB_IN_GA(T26, T28)
PB_IN_GA(T26, T28) → U2_GA(T26, T28, lessA_in_g(T26))
PB_IN_GA(T26, T28) → LESSA_IN_G(T26)
LESSA_IN_G(s(T31)) → U1_G(T31, lessA_in_g(T31))
LESSA_IN_G(s(T31)) → LESSA_IN_G(T31)
U2_GA(T26, T28, lessA_out_g(T26)) → U3_GA(T26, T28, deleteC_in_gga(T26, void, T28))
U2_GA(T26, T28, lessA_out_g(T26)) → DELETEC_IN_GGA(T26, void, T28)
DELETEC_IN_GGA(T38, tree(T38, void, void), tree(T38, void, T40)) → U12_GGA(T38, T40, pB_in_ga(T38, T40))
DELETEC_IN_GGA(T38, tree(T38, void, void), tree(T38, void, T40)) → PB_IN_GA(T38, T40)
DELETEC_IN_GGA(s(T50), tree(s(T50), void, void), tree(s(T50), T45, void)) → U13_GGA(T50, T45, pD_in_ga(T50, T45))
DELETEC_IN_GGA(s(T50), tree(s(T50), void, void), tree(s(T50), T45, void)) → PD_IN_GA(T50, T45)
PD_IN_GA(T50, T45) → U4_GA(T50, T45, lessA_in_g(T50))
PD_IN_GA(T50, T45) → LESSA_IN_G(T50)
U4_GA(T50, T45, lessA_out_g(T50)) → U5_GA(T50, T45, deleteC_in_gga(s(T50), void, T45))
U4_GA(T50, T45, lessA_out_g(T50)) → DELETEC_IN_GGA(s(T50), void, T45)
DELETEC_IN_GGA(T57, tree(T57, void, void), tree(T57, void, T59)) → U14_GGA(T57, T59, pB_in_ga(T57, T59))
DELETEC_IN_GGA(s(T67), tree(s(T67), void, void), tree(s(T67), void, T64)) → U15_GGA(T67, T64, pD_in_ga(T67, T64))
DELETEC_IN_GGA(s(T67), tree(s(T67), void, void), tree(s(T67), void, T64)) → PD_IN_GA(T67, T64)
DELETEC_IN_GGA(T72, tree(T72, void, tree(T112, T113, T114)), tree(T118, void, tree(T112, T119, T117))) → U16_GGA(T72, T112, T113, T114, T118, T119, T117, delminE_in_gaa(T113, T118, T119))
DELETEC_IN_GGA(T72, tree(T72, void, tree(T112, T113, T114)), tree(T118, void, tree(T112, T119, T117))) → DELMINE_IN_GAA(T113, T118, T119)
DELMINE_IN_GAA(tree(T146, T147, T148), T152, tree(T146, T153, T151)) → U6_GAA(T146, T147, T148, T152, T153, T151, delminE_in_gaa(T147, T152, T153))
DELMINE_IN_GAA(tree(T146, T147, T148), T152, tree(T146, T153, T151)) → DELMINE_IN_GAA(T147, T152, T153)
DELETEC_IN_GGA(T170, tree(T170, void, T171), tree(T170, T173, T171)) → U17_GGA(T170, T171, T173, pB_in_ga(T170, T173))
DELETEC_IN_GGA(T170, tree(T170, void, T171), tree(T170, T173, T171)) → PB_IN_GA(T170, T173)
DELETEC_IN_GGA(T180, tree(T180, void, T181), tree(T180, void, T183)) → U18_GGA(T180, T181, T183, pF_in_gga(T180, T181, T183))
DELETEC_IN_GGA(T180, tree(T180, void, T181), tree(T180, void, T183)) → PF_IN_GGA(T180, T181, T183)
PF_IN_GGA(T180, T181, T183) → U7_GGA(T180, T181, T183, lessA_in_g(T180))
PF_IN_GGA(T180, T181, T183) → LESSA_IN_G(T180)
U7_GGA(T180, T181, T183, lessA_out_g(T180)) → U8_GGA(T180, T181, T183, deleteC_in_gga(T180, T181, T183))
U7_GGA(T180, T181, T183, lessA_out_g(T180)) → DELETEC_IN_GGA(T180, T181, T183)
DELETEC_IN_GGA(s(T199), tree(s(T199), void, T192), tree(s(T199), T194, T192)) → U19_GGA(T199, T192, T194, lessA_in_g(T199))
DELETEC_IN_GGA(s(T199), tree(s(T199), void, T192), tree(s(T199), T194, T192)) → LESSA_IN_G(T199)
U19_GGA(T199, T192, T194, lessA_out_g(T199)) → U20_GGA(T199, T192, T194, deleteC_in_gga(s(T199), void, T194))
U19_GGA(T199, T192, T194, lessA_out_g(T199)) → DELETEC_IN_GGA(s(T199), void, T194)
DELETEC_IN_GGA(T208, tree(T208, void, T209), tree(T208, void, T211)) → U21_GGA(T208, T209, T211, pF_in_gga(T208, T209, T211))
DELETEC_IN_GGA(s(T221), tree(s(T221), void, T216), tree(s(T221), void, T218)) → U22_GGA(T221, T216, T218, lessA_in_g(T221))
DELETEC_IN_GGA(s(T221), tree(s(T221), void, T216), tree(s(T221), void, T218)) → LESSA_IN_G(T221)
U22_GGA(T221, T216, T218, lessA_out_g(T221)) → U23_GGA(T221, T216, T218, deleteC_in_gga(s(T221), T216, T218))
U22_GGA(T221, T216, T218, lessA_out_g(T221)) → DELETEC_IN_GGA(s(T221), T216, T218)
DELETEC_IN_GGA(T252, tree(T252, T253, void), tree(T252, T255, void)) → U24_GGA(T252, T253, T255, lessA_in_g(T252))
DELETEC_IN_GGA(T252, tree(T252, T253, void), tree(T252, T255, void)) → LESSA_IN_G(T252)
U24_GGA(T252, T253, T255, lessA_out_g(T252)) → U25_GGA(T252, T253, T255, deleteC_in_gga(T252, T253, T255))
U24_GGA(T252, T253, T255, lessA_out_g(T252)) → DELETEC_IN_GGA(T252, T253, T255)
DELETEC_IN_GGA(T266, tree(T266, T267, void), tree(T266, T267, T269)) → U26_GGA(T266, T267, T269, pB_in_ga(T266, T269))
DELETEC_IN_GGA(T266, tree(T266, T267, void), tree(T266, T267, T269)) → PB_IN_GA(T266, T269)
DELETEC_IN_GGA(s(T281), tree(s(T281), T274, void), tree(s(T281), T276, void)) → U27_GGA(T281, T274, T276, lessA_in_g(T281))
DELETEC_IN_GGA(s(T281), tree(s(T281), T274, void), tree(s(T281), T276, void)) → LESSA_IN_G(T281)
U27_GGA(T281, T274, T276, lessA_out_g(T281)) → U28_GGA(T281, T274, T276, deleteC_in_gga(s(T281), T274, T276))
U27_GGA(T281, T274, T276, lessA_out_g(T281)) → DELETEC_IN_GGA(s(T281), T274, T276)
DELETEC_IN_GGA(T292, tree(T292, T293, void), tree(T292, T293, T295)) → U29_GGA(T292, T293, T295, pB_in_ga(T292, T295))
DELETEC_IN_GGA(s(T305), tree(s(T305), T300, void), tree(s(T305), T300, T302)) → U30_GGA(T305, T300, T302, lessA_in_g(T305))
DELETEC_IN_GGA(s(T305), tree(s(T305), T300, void), tree(s(T305), T300, T302)) → LESSA_IN_G(T305)
U30_GGA(T305, T300, T302, lessA_out_g(T305)) → U31_GGA(T305, T300, T302, deleteC_in_gga(s(T305), void, T302))
U30_GGA(T305, T300, T302, lessA_out_g(T305)) → DELETEC_IN_GGA(s(T305), void, T302)
DELETEC_IN_GGA(T313, tree(T313, T314, tree(T354, T355, T356)), tree(T360, T314, tree(T354, T361, T359))) → U32_GGA(T313, T314, T354, T355, T356, T360, T361, T359, delminE_in_gaa(T355, T360, T361))
DELETEC_IN_GGA(T313, tree(T313, T314, tree(T354, T355, T356)), tree(T360, T314, tree(T354, T361, T359))) → DELMINE_IN_GAA(T355, T360, T361)
DELETEC_IN_GGA(T382, tree(T382, T383, T384), tree(T382, T386, T384)) → U33_GGA(T382, T383, T384, T386, lessA_in_g(T382))
DELETEC_IN_GGA(T382, tree(T382, T383, T384), tree(T382, T386, T384)) → LESSA_IN_G(T382)
U33_GGA(T382, T383, T384, T386, lessA_out_g(T382)) → U34_GGA(T382, T383, T384, T386, deleteC_in_gga(T382, T383, T386))
U33_GGA(T382, T383, T384, T386, lessA_out_g(T382)) → DELETEC_IN_GGA(T382, T383, T386)
DELETEC_IN_GGA(T399, tree(T399, T400, T401), tree(T399, T400, T403)) → U35_GGA(T399, T400, T401, T403, lessA_in_g(T399))
DELETEC_IN_GGA(T399, tree(T399, T400, T401), tree(T399, T400, T403)) → LESSA_IN_G(T399)
U35_GGA(T399, T400, T401, T403, lessA_out_g(T399)) → U36_GGA(T399, T400, T401, T403, deleteC_in_gga(T399, T401, T403))
U35_GGA(T399, T400, T401, T403, lessA_out_g(T399)) → DELETEC_IN_GGA(T399, T401, T403)
DELETEC_IN_GGA(0, tree(s(T423), T415, T416), tree(s(T423), T418, T416)) → U37_GGA(T423, T415, T416, T418, deleteC_in_gga(0, T415, T418))
DELETEC_IN_GGA(0, tree(s(T423), T415, T416), tree(s(T423), T418, T416)) → DELETEC_IN_GGA(0, T415, T418)
DELETEC_IN_GGA(s(T434), tree(s(T435), T415, T416), tree(s(T435), T418, T416)) → U38_GGA(T434, T435, T415, T416, T418, lessH_in_gg(T434, T435))
DELETEC_IN_GGA(s(T434), tree(s(T435), T415, T416), tree(s(T435), T418, T416)) → LESSH_IN_GG(T434, T435)
LESSH_IN_GG(s(s(s(s(s(s(s(T527))))))), s(s(s(s(s(s(s(T528)))))))) → U10_GG(T527, T528, lessG_in_gg(T527, T528))
LESSH_IN_GG(s(s(s(s(s(s(s(T527))))))), s(s(s(s(s(s(s(T528)))))))) → LESSG_IN_GG(T527, T528)
LESSG_IN_GG(s(T544), s(T545)) → U9_GG(T544, T545, lessG_in_gg(T544, T545))
LESSG_IN_GG(s(T544), s(T545)) → LESSG_IN_GG(T544, T545)
U38_GGA(T434, T435, T415, T416, T418, lessH_out_gg(T434, T435)) → U39_GGA(T434, T435, T415, T416, T418, deleteC_in_gga(s(T434), T415, T418))
U38_GGA(T434, T435, T415, T416, T418, lessH_out_gg(T434, T435)) → DELETEC_IN_GGA(s(T434), T415, T418)
DELETEC_IN_GGA(T562, tree(T563, T564, T565), tree(T563, T564, T567)) → U40_GGA(T562, T563, T564, T565, T567, lessG_in_gg(T563, T562))
DELETEC_IN_GGA(T562, tree(T563, T564, T565), tree(T563, T564, T567)) → LESSG_IN_GG(T563, T562)
U40_GGA(T562, T563, T564, T565, T567, lessG_out_gg(T563, T562)) → U41_GGA(T562, T563, T564, T565, T567, deleteC_in_gga(T562, T565, T567))
U40_GGA(T562, T563, T564, T565, T567, lessG_out_gg(T563, T562)) → DELETEC_IN_GGA(T562, T565, T567)
DELETEC_IN_GGA(s(T591), tree(0, T583, T584), tree(0, T583, T586)) → U42_GGA(T591, T583, T584, T586, deleteC_in_gga(s(T591), T584, T586))
DELETEC_IN_GGA(s(T591), tree(0, T583, T584), tree(0, T583, T586)) → DELETEC_IN_GGA(s(T591), T584, T586)
DELETEC_IN_GGA(s(T601), tree(s(T600), T583, T584), tree(s(T600), T583, T586)) → U43_GGA(T601, T600, T583, T584, T586, lessG_in_gg(T600, T601))
DELETEC_IN_GGA(s(T601), tree(s(T600), T583, T584), tree(s(T600), T583, T586)) → LESSG_IN_GG(T600, T601)
U43_GGA(T601, T600, T583, T584, T586, lessG_out_gg(T600, T601)) → U44_GGA(T601, T600, T583, T584, T586, deleteC_in_gga(s(T601), T584, T586))
U43_GGA(T601, T600, T583, T584, T586, lessG_out_gg(T600, T601)) → DELETEC_IN_GGA(s(T601), T584, T586)

The TRS R consists of the following rules:

deleteC_in_gga(T6, tree(T6, void, T7), T7) → deleteC_out_gga(T6, tree(T6, void, T7), T7)
deleteC_in_gga(T9, tree(T9, void, void), void) → deleteC_out_gga(T9, tree(T9, void, void), void)
deleteC_in_gga(T26, tree(T26, void, void), tree(T26, T28, void)) → U11_gga(T26, T28, pB_in_ga(T26, T28))
pB_in_ga(T26, T28) → U2_ga(T26, T28, lessA_in_g(T26))
lessA_in_g(s(T31)) → U1_g(T31, lessA_in_g(T31))
U1_g(T31, lessA_out_g(T31)) → lessA_out_g(s(T31))
U2_ga(T26, T28, lessA_out_g(T26)) → pB_out_ga(T26, T28)
U2_ga(T26, T28, lessA_out_g(T26)) → U3_ga(T26, T28, deleteC_in_gga(T26, void, T28))
deleteC_in_gga(T38, tree(T38, void, void), tree(T38, void, T40)) → U12_gga(T38, T40, pB_in_ga(T38, T40))
U12_gga(T38, T40, pB_out_ga(T38, T40)) → deleteC_out_gga(T38, tree(T38, void, void), tree(T38, void, T40))
deleteC_in_gga(s(T50), tree(s(T50), void, void), tree(s(T50), T45, void)) → U13_gga(T50, T45, pD_in_ga(T50, T45))
pD_in_ga(T50, T45) → U4_ga(T50, T45, lessA_in_g(T50))
U4_ga(T50, T45, lessA_out_g(T50)) → pD_out_ga(T50, T45)
U4_ga(T50, T45, lessA_out_g(T50)) → U5_ga(T50, T45, deleteC_in_gga(s(T50), void, T45))
deleteC_in_gga(T57, tree(T57, void, void), tree(T57, void, T59)) → U14_gga(T57, T59, pB_in_ga(T57, T59))
U14_gga(T57, T59, pB_out_ga(T57, T59)) → deleteC_out_gga(T57, tree(T57, void, void), tree(T57, void, T59))
deleteC_in_gga(s(T67), tree(s(T67), void, void), tree(s(T67), void, T64)) → U15_gga(T67, T64, pD_in_ga(T67, T64))
U15_gga(T67, T64, pD_out_ga(T67, T64)) → deleteC_out_gga(s(T67), tree(s(T67), void, void), tree(s(T67), void, T64))
deleteC_in_gga(T72, tree(T72, void, tree(T86, void, T87)), tree(T86, void, T87)) → deleteC_out_gga(T72, tree(T72, void, tree(T86, void, T87)), tree(T86, void, T87))
deleteC_in_gga(T72, tree(T72, void, tree(T112, T113, T114)), tree(T118, void, tree(T112, T119, T117))) → U16_gga(T72, T112, T113, T114, T118, T119, T117, delminE_in_gaa(T113, T118, T119))
delminE_in_gaa(tree(T132, void, T133), T132, T133) → delminE_out_gaa(tree(T132, void, T133), T132, T133)
delminE_in_gaa(tree(T146, T147, T148), T152, tree(T146, T153, T151)) → U6_gaa(T146, T147, T148, T152, T153, T151, delminE_in_gaa(T147, T152, T153))
U6_gaa(T146, T147, T148, T152, T153, T151, delminE_out_gaa(T147, T152, T153)) → delminE_out_gaa(tree(T146, T147, T148), T152, tree(T146, T153, T151))
U16_gga(T72, T112, T113, T114, T118, T119, T117, delminE_out_gaa(T113, T118, T119)) → deleteC_out_gga(T72, tree(T72, void, tree(T112, T113, T114)), tree(T118, void, tree(T112, T119, T117)))
deleteC_in_gga(T170, tree(T170, void, T171), tree(T170, T173, T171)) → U17_gga(T170, T171, T173, pB_in_ga(T170, T173))
U17_gga(T170, T171, T173, pB_out_ga(T170, T173)) → deleteC_out_gga(T170, tree(T170, void, T171), tree(T170, T173, T171))
deleteC_in_gga(T180, tree(T180, void, T181), tree(T180, void, T183)) → U18_gga(T180, T181, T183, pF_in_gga(T180, T181, T183))
pF_in_gga(T180, T181, T183) → U7_gga(T180, T181, T183, lessA_in_g(T180))
U7_gga(T180, T181, T183, lessA_out_g(T180)) → pF_out_gga(T180, T181, T183)
U7_gga(T180, T181, T183, lessA_out_g(T180)) → U8_gga(T180, T181, T183, deleteC_in_gga(T180, T181, T183))
deleteC_in_gga(s(T199), tree(s(T199), void, T192), tree(s(T199), T194, T192)) → U19_gga(T199, T192, T194, lessA_in_g(T199))
U19_gga(T199, T192, T194, lessA_out_g(T199)) → deleteC_out_gga(s(T199), tree(s(T199), void, T192), tree(s(T199), T194, T192))
U19_gga(T199, T192, T194, lessA_out_g(T199)) → U20_gga(T199, T192, T194, deleteC_in_gga(s(T199), void, T194))
deleteC_in_gga(T208, tree(T208, void, T209), tree(T208, void, T211)) → U21_gga(T208, T209, T211, pF_in_gga(T208, T209, T211))
U21_gga(T208, T209, T211, pF_out_gga(T208, T209, T211)) → deleteC_out_gga(T208, tree(T208, void, T209), tree(T208, void, T211))
deleteC_in_gga(s(T221), tree(s(T221), void, T216), tree(s(T221), void, T218)) → U22_gga(T221, T216, T218, lessA_in_g(T221))
U22_gga(T221, T216, T218, lessA_out_g(T221)) → deleteC_out_gga(s(T221), tree(s(T221), void, T216), tree(s(T221), void, T218))
U22_gga(T221, T216, T218, lessA_out_g(T221)) → U23_gga(T221, T216, T218, deleteC_in_gga(s(T221), T216, T218))
deleteC_in_gga(T228, tree(T228, T229, void), T229) → deleteC_out_gga(T228, tree(T228, T229, void), T229)
deleteC_in_gga(T252, tree(T252, T253, void), tree(T252, T255, void)) → U24_gga(T252, T253, T255, lessA_in_g(T252))
U24_gga(T252, T253, T255, lessA_out_g(T252)) → deleteC_out_gga(T252, tree(T252, T253, void), tree(T252, T255, void))
U24_gga(T252, T253, T255, lessA_out_g(T252)) → U25_gga(T252, T253, T255, deleteC_in_gga(T252, T253, T255))
deleteC_in_gga(T266, tree(T266, T267, void), tree(T266, T267, T269)) → U26_gga(T266, T267, T269, pB_in_ga(T266, T269))
U26_gga(T266, T267, T269, pB_out_ga(T266, T269)) → deleteC_out_gga(T266, tree(T266, T267, void), tree(T266, T267, T269))
deleteC_in_gga(s(T281), tree(s(T281), T274, void), tree(s(T281), T276, void)) → U27_gga(T281, T274, T276, lessA_in_g(T281))
U27_gga(T281, T274, T276, lessA_out_g(T281)) → deleteC_out_gga(s(T281), tree(s(T281), T274, void), tree(s(T281), T276, void))
U27_gga(T281, T274, T276, lessA_out_g(T281)) → U28_gga(T281, T274, T276, deleteC_in_gga(s(T281), T274, T276))
deleteC_in_gga(T292, tree(T292, T293, void), tree(T292, T293, T295)) → U29_gga(T292, T293, T295, pB_in_ga(T292, T295))
U29_gga(T292, T293, T295, pB_out_ga(T292, T295)) → deleteC_out_gga(T292, tree(T292, T293, void), tree(T292, T293, T295))
deleteC_in_gga(s(T305), tree(s(T305), T300, void), tree(s(T305), T300, T302)) → U30_gga(T305, T300, T302, lessA_in_g(T305))
U30_gga(T305, T300, T302, lessA_out_g(T305)) → deleteC_out_gga(s(T305), tree(s(T305), T300, void), tree(s(T305), T300, T302))
U30_gga(T305, T300, T302, lessA_out_g(T305)) → U31_gga(T305, T300, T302, deleteC_in_gga(s(T305), void, T302))
deleteC_in_gga(T313, tree(T313, T314, tree(T328, void, T329)), tree(T328, T314, T329)) → deleteC_out_gga(T313, tree(T313, T314, tree(T328, void, T329)), tree(T328, T314, T329))
deleteC_in_gga(T313, tree(T313, T314, tree(T354, T355, T356)), tree(T360, T314, tree(T354, T361, T359))) → U32_gga(T313, T314, T354, T355, T356, T360, T361, T359, delminE_in_gaa(T355, T360, T361))
U32_gga(T313, T314, T354, T355, T356, T360, T361, T359, delminE_out_gaa(T355, T360, T361)) → deleteC_out_gga(T313, tree(T313, T314, tree(T354, T355, T356)), tree(T360, T314, tree(T354, T361, T359)))
deleteC_in_gga(T382, tree(T382, T383, T384), tree(T382, T386, T384)) → U33_gga(T382, T383, T384, T386, lessA_in_g(T382))
U33_gga(T382, T383, T384, T386, lessA_out_g(T382)) → deleteC_out_gga(T382, tree(T382, T383, T384), tree(T382, T386, T384))
U33_gga(T382, T383, T384, T386, lessA_out_g(T382)) → U34_gga(T382, T383, T384, T386, deleteC_in_gga(T382, T383, T386))
deleteC_in_gga(T399, tree(T399, T400, T401), tree(T399, T400, T403)) → U35_gga(T399, T400, T401, T403, lessA_in_g(T399))
U35_gga(T399, T400, T401, T403, lessA_out_g(T399)) → deleteC_out_gga(T399, tree(T399, T400, T401), tree(T399, T400, T403))
U35_gga(T399, T400, T401, T403, lessA_out_g(T399)) → U36_gga(T399, T400, T401, T403, deleteC_in_gga(T399, T401, T403))
deleteC_in_gga(0, tree(s(T423), T415, T416), tree(s(T423), T418, T416)) → U37_gga(T423, T415, T416, T418, deleteC_in_gga(0, T415, T418))
deleteC_in_gga(s(T434), tree(s(T435), T415, T416), tree(s(T435), T418, T416)) → U38_gga(T434, T435, T415, T416, T418, lessH_in_gg(T434, T435))
lessH_in_gg(0, s(T444)) → lessH_out_gg(0, s(T444))
lessH_in_gg(s(0), s(s(T457))) → lessH_out_gg(s(0), s(s(T457)))
lessH_in_gg(s(s(0)), s(s(s(T470)))) → lessH_out_gg(s(s(0)), s(s(s(T470))))
lessH_in_gg(s(s(s(0))), s(s(s(s(T483))))) → lessH_out_gg(s(s(s(0))), s(s(s(s(T483)))))
lessH_in_gg(s(s(s(s(0)))), s(s(s(s(s(T496)))))) → lessH_out_gg(s(s(s(s(0)))), s(s(s(s(s(T496))))))
lessH_in_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T509))))))) → lessH_out_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T509)))))))
lessH_in_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T522)))))))) → lessH_out_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T522))))))))
lessH_in_gg(s(s(s(s(s(s(s(T527))))))), s(s(s(s(s(s(s(T528)))))))) → U10_gg(T527, T528, lessG_in_gg(T527, T528))
lessG_in_gg(0, s(T539)) → lessG_out_gg(0, s(T539))
lessG_in_gg(s(T544), s(T545)) → U9_gg(T544, T545, lessG_in_gg(T544, T545))
U9_gg(T544, T545, lessG_out_gg(T544, T545)) → lessG_out_gg(s(T544), s(T545))
U10_gg(T527, T528, lessG_out_gg(T527, T528)) → lessH_out_gg(s(s(s(s(s(s(s(T527))))))), s(s(s(s(s(s(s(T528))))))))
U38_gga(T434, T435, T415, T416, T418, lessH_out_gg(T434, T435)) → deleteC_out_gga(s(T434), tree(s(T435), T415, T416), tree(s(T435), T418, T416))
U38_gga(T434, T435, T415, T416, T418, lessH_out_gg(T434, T435)) → U39_gga(T434, T435, T415, T416, T418, deleteC_in_gga(s(T434), T415, T418))
deleteC_in_gga(T562, tree(T563, T564, T565), tree(T563, T564, T567)) → U40_gga(T562, T563, T564, T565, T567, lessG_in_gg(T563, T562))
U40_gga(T562, T563, T564, T565, T567, lessG_out_gg(T563, T562)) → deleteC_out_gga(T562, tree(T563, T564, T565), tree(T563, T564, T567))
U40_gga(T562, T563, T564, T565, T567, lessG_out_gg(T563, T562)) → U41_gga(T562, T563, T564, T565, T567, deleteC_in_gga(T562, T565, T567))
deleteC_in_gga(s(T591), tree(0, T583, T584), tree(0, T583, T586)) → U42_gga(T591, T583, T584, T586, deleteC_in_gga(s(T591), T584, T586))
deleteC_in_gga(s(T601), tree(s(T600), T583, T584), tree(s(T600), T583, T586)) → U43_gga(T601, T600, T583, T584, T586, lessG_in_gg(T600, T601))
U43_gga(T601, T600, T583, T584, T586, lessG_out_gg(T600, T601)) → deleteC_out_gga(s(T601), tree(s(T600), T583, T584), tree(s(T600), T583, T586))
U43_gga(T601, T600, T583, T584, T586, lessG_out_gg(T600, T601)) → U44_gga(T601, T600, T583, T584, T586, deleteC_in_gga(s(T601), T584, T586))
U44_gga(T601, T600, T583, T584, T586, deleteC_out_gga(s(T601), T584, T586)) → deleteC_out_gga(s(T601), tree(s(T600), T583, T584), tree(s(T600), T583, T586))
U42_gga(T591, T583, T584, T586, deleteC_out_gga(s(T591), T584, T586)) → deleteC_out_gga(s(T591), tree(0, T583, T584), tree(0, T583, T586))
U41_gga(T562, T563, T564, T565, T567, deleteC_out_gga(T562, T565, T567)) → deleteC_out_gga(T562, tree(T563, T564, T565), tree(T563, T564, T567))
U39_gga(T434, T435, T415, T416, T418, deleteC_out_gga(s(T434), T415, T418)) → deleteC_out_gga(s(T434), tree(s(T435), T415, T416), tree(s(T435), T418, T416))
U37_gga(T423, T415, T416, T418, deleteC_out_gga(0, T415, T418)) → deleteC_out_gga(0, tree(s(T423), T415, T416), tree(s(T423), T418, T416))
U36_gga(T399, T400, T401, T403, deleteC_out_gga(T399, T401, T403)) → deleteC_out_gga(T399, tree(T399, T400, T401), tree(T399, T400, T403))
U34_gga(T382, T383, T384, T386, deleteC_out_gga(T382, T383, T386)) → deleteC_out_gga(T382, tree(T382, T383, T384), tree(T382, T386, T384))
U31_gga(T305, T300, T302, deleteC_out_gga(s(T305), void, T302)) → deleteC_out_gga(s(T305), tree(s(T305), T300, void), tree(s(T305), T300, T302))
U28_gga(T281, T274, T276, deleteC_out_gga(s(T281), T274, T276)) → deleteC_out_gga(s(T281), tree(s(T281), T274, void), tree(s(T281), T276, void))
U25_gga(T252, T253, T255, deleteC_out_gga(T252, T253, T255)) → deleteC_out_gga(T252, tree(T252, T253, void), tree(T252, T255, void))
U23_gga(T221, T216, T218, deleteC_out_gga(s(T221), T216, T218)) → deleteC_out_gga(s(T221), tree(s(T221), void, T216), tree(s(T221), void, T218))
U20_gga(T199, T192, T194, deleteC_out_gga(s(T199), void, T194)) → deleteC_out_gga(s(T199), tree(s(T199), void, T192), tree(s(T199), T194, T192))
U8_gga(T180, T181, T183, deleteC_out_gga(T180, T181, T183)) → pF_out_gga(T180, T181, T183)
U18_gga(T180, T181, T183, pF_out_gga(T180, T181, T183)) → deleteC_out_gga(T180, tree(T180, void, T181), tree(T180, void, T183))
U5_ga(T50, T45, deleteC_out_gga(s(T50), void, T45)) → pD_out_ga(T50, T45)
U13_gga(T50, T45, pD_out_ga(T50, T45)) → deleteC_out_gga(s(T50), tree(s(T50), void, void), tree(s(T50), T45, void))
U3_ga(T26, T28, deleteC_out_gga(T26, void, T28)) → pB_out_ga(T26, T28)
U11_gga(T26, T28, pB_out_ga(T26, T28)) → deleteC_out_gga(T26, tree(T26, void, void), tree(T26, T28, void))

The argument filtering Pi contains the following mapping:
deleteC_in_gga(x1, x2, x3)  =  deleteC_in_gga(x1, x2)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
void  =  void
deleteC_out_gga(x1, x2, x3)  =  deleteC_out_gga
U11_gga(x1, x2, x3)  =  U11_gga(x3)
pB_in_ga(x1, x2)  =  pB_in_ga(x1)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
lessA_in_g(x1)  =  lessA_in_g(x1)
s(x1)  =  s(x1)
U1_g(x1, x2)  =  U1_g(x2)
lessA_out_g(x1)  =  lessA_out_g
pB_out_ga(x1, x2)  =  pB_out_ga
U3_ga(x1, x2, x3)  =  U3_ga(x3)
U12_gga(x1, x2, x3)  =  U12_gga(x3)
U13_gga(x1, x2, x3)  =  U13_gga(x3)
pD_in_ga(x1, x2)  =  pD_in_ga(x1)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
pD_out_ga(x1, x2)  =  pD_out_ga
U5_ga(x1, x2, x3)  =  U5_ga(x3)
U14_gga(x1, x2, x3)  =  U14_gga(x3)
U15_gga(x1, x2, x3)  =  U15_gga(x3)
U16_gga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U16_gga(x8)
delminE_in_gaa(x1, x2, x3)  =  delminE_in_gaa(x1)
delminE_out_gaa(x1, x2, x3)  =  delminE_out_gaa(x2)
U6_gaa(x1, x2, x3, x4, x5, x6, x7)  =  U6_gaa(x7)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x4)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x4)
pF_in_gga(x1, x2, x3)  =  pF_in_gga(x1, x2)
U7_gga(x1, x2, x3, x4)  =  U7_gga(x1, x2, x4)
pF_out_gga(x1, x2, x3)  =  pF_out_gga
U8_gga(x1, x2, x3, x4)  =  U8_gga(x4)
U19_gga(x1, x2, x3, x4)  =  U19_gga(x1, x4)
U20_gga(x1, x2, x3, x4)  =  U20_gga(x4)
U21_gga(x1, x2, x3, x4)  =  U21_gga(x4)
U22_gga(x1, x2, x3, x4)  =  U22_gga(x1, x2, x4)
U23_gga(x1, x2, x3, x4)  =  U23_gga(x4)
U24_gga(x1, x2, x3, x4)  =  U24_gga(x1, x2, x4)
U25_gga(x1, x2, x3, x4)  =  U25_gga(x4)
U26_gga(x1, x2, x3, x4)  =  U26_gga(x4)
U27_gga(x1, x2, x3, x4)  =  U27_gga(x1, x2, x4)
U28_gga(x1, x2, x3, x4)  =  U28_gga(x4)
U29_gga(x1, x2, x3, x4)  =  U29_gga(x4)
U30_gga(x1, x2, x3, x4)  =  U30_gga(x1, x4)
U31_gga(x1, x2, x3, x4)  =  U31_gga(x4)
U32_gga(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U32_gga(x9)
U33_gga(x1, x2, x3, x4, x5)  =  U33_gga(x1, x2, x5)
U34_gga(x1, x2, x3, x4, x5)  =  U34_gga(x5)
U35_gga(x1, x2, x3, x4, x5)  =  U35_gga(x1, x3, x5)
U36_gga(x1, x2, x3, x4, x5)  =  U36_gga(x5)
0  =  0
U37_gga(x1, x2, x3, x4, x5)  =  U37_gga(x5)
U38_gga(x1, x2, x3, x4, x5, x6)  =  U38_gga(x1, x3, x6)
lessH_in_gg(x1, x2)  =  lessH_in_gg(x1, x2)
lessH_out_gg(x1, x2)  =  lessH_out_gg
U10_gg(x1, x2, x3)  =  U10_gg(x3)
lessG_in_gg(x1, x2)  =  lessG_in_gg(x1, x2)
lessG_out_gg(x1, x2)  =  lessG_out_gg
U9_gg(x1, x2, x3)  =  U9_gg(x3)
U39_gga(x1, x2, x3, x4, x5, x6)  =  U39_gga(x6)
U40_gga(x1, x2, x3, x4, x5, x6)  =  U40_gga(x1, x4, x6)
U41_gga(x1, x2, x3, x4, x5, x6)  =  U41_gga(x6)
U42_gga(x1, x2, x3, x4, x5)  =  U42_gga(x5)
U43_gga(x1, x2, x3, x4, x5, x6)  =  U43_gga(x1, x4, x6)
U44_gga(x1, x2, x3, x4, x5, x6)  =  U44_gga(x6)
DELETEC_IN_GGA(x1, x2, x3)  =  DELETEC_IN_GGA(x1, x2)
U11_GGA(x1, x2, x3)  =  U11_GGA(x3)
PB_IN_GA(x1, x2)  =  PB_IN_GA(x1)
U2_GA(x1, x2, x3)  =  U2_GA(x1, x3)
LESSA_IN_G(x1)  =  LESSA_IN_G(x1)
U1_G(x1, x2)  =  U1_G(x2)
U3_GA(x1, x2, x3)  =  U3_GA(x3)
U12_GGA(x1, x2, x3)  =  U12_GGA(x3)
U13_GGA(x1, x2, x3)  =  U13_GGA(x3)
PD_IN_GA(x1, x2)  =  PD_IN_GA(x1)
U4_GA(x1, x2, x3)  =  U4_GA(x1, x3)
U5_GA(x1, x2, x3)  =  U5_GA(x3)
U14_GGA(x1, x2, x3)  =  U14_GGA(x3)
U15_GGA(x1, x2, x3)  =  U15_GGA(x3)
U16_GGA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U16_GGA(x8)
DELMINE_IN_GAA(x1, x2, x3)  =  DELMINE_IN_GAA(x1)
U6_GAA(x1, x2, x3, x4, x5, x6, x7)  =  U6_GAA(x7)
U17_GGA(x1, x2, x3, x4)  =  U17_GGA(x4)
U18_GGA(x1, x2, x3, x4)  =  U18_GGA(x4)
PF_IN_GGA(x1, x2, x3)  =  PF_IN_GGA(x1, x2)
U7_GGA(x1, x2, x3, x4)  =  U7_GGA(x1, x2, x4)
U8_GGA(x1, x2, x3, x4)  =  U8_GGA(x4)
U19_GGA(x1, x2, x3, x4)  =  U19_GGA(x1, x4)
U20_GGA(x1, x2, x3, x4)  =  U20_GGA(x4)
U21_GGA(x1, x2, x3, x4)  =  U21_GGA(x4)
U22_GGA(x1, x2, x3, x4)  =  U22_GGA(x1, x2, x4)
U23_GGA(x1, x2, x3, x4)  =  U23_GGA(x4)
U24_GGA(x1, x2, x3, x4)  =  U24_GGA(x1, x2, x4)
U25_GGA(x1, x2, x3, x4)  =  U25_GGA(x4)
U26_GGA(x1, x2, x3, x4)  =  U26_GGA(x4)
U27_GGA(x1, x2, x3, x4)  =  U27_GGA(x1, x2, x4)
U28_GGA(x1, x2, x3, x4)  =  U28_GGA(x4)
U29_GGA(x1, x2, x3, x4)  =  U29_GGA(x4)
U30_GGA(x1, x2, x3, x4)  =  U30_GGA(x1, x4)
U31_GGA(x1, x2, x3, x4)  =  U31_GGA(x4)
U32_GGA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U32_GGA(x9)
U33_GGA(x1, x2, x3, x4, x5)  =  U33_GGA(x1, x2, x5)
U34_GGA(x1, x2, x3, x4, x5)  =  U34_GGA(x5)
U35_GGA(x1, x2, x3, x4, x5)  =  U35_GGA(x1, x3, x5)
U36_GGA(x1, x2, x3, x4, x5)  =  U36_GGA(x5)
U37_GGA(x1, x2, x3, x4, x5)  =  U37_GGA(x5)
U38_GGA(x1, x2, x3, x4, x5, x6)  =  U38_GGA(x1, x3, x6)
LESSH_IN_GG(x1, x2)  =  LESSH_IN_GG(x1, x2)
U10_GG(x1, x2, x3)  =  U10_GG(x3)
LESSG_IN_GG(x1, x2)  =  LESSG_IN_GG(x1, x2)
U9_GG(x1, x2, x3)  =  U9_GG(x3)
U39_GGA(x1, x2, x3, x4, x5, x6)  =  U39_GGA(x6)
U40_GGA(x1, x2, x3, x4, x5, x6)  =  U40_GGA(x1, x4, x6)
U41_GGA(x1, x2, x3, x4, x5, x6)  =  U41_GGA(x6)
U42_GGA(x1, x2, x3, x4, x5)  =  U42_GGA(x5)
U43_GGA(x1, x2, x3, x4, x5, x6)  =  U43_GGA(x1, x4, x6)
U44_GGA(x1, x2, x3, x4, x5, x6)  =  U44_GGA(x6)

We have to consider all (P,R,Pi)-chains

(7) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 4 SCCs with 61 less nodes.

(8) Complex Obligation (AND)

(9) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

LESSG_IN_GG(s(T544), s(T545)) → LESSG_IN_GG(T544, T545)

The TRS R consists of the following rules:

deleteC_in_gga(T6, tree(T6, void, T7), T7) → deleteC_out_gga(T6, tree(T6, void, T7), T7)
deleteC_in_gga(T9, tree(T9, void, void), void) → deleteC_out_gga(T9, tree(T9, void, void), void)
deleteC_in_gga(T26, tree(T26, void, void), tree(T26, T28, void)) → U11_gga(T26, T28, pB_in_ga(T26, T28))
pB_in_ga(T26, T28) → U2_ga(T26, T28, lessA_in_g(T26))
lessA_in_g(s(T31)) → U1_g(T31, lessA_in_g(T31))
U1_g(T31, lessA_out_g(T31)) → lessA_out_g(s(T31))
U2_ga(T26, T28, lessA_out_g(T26)) → pB_out_ga(T26, T28)
U2_ga(T26, T28, lessA_out_g(T26)) → U3_ga(T26, T28, deleteC_in_gga(T26, void, T28))
deleteC_in_gga(T38, tree(T38, void, void), tree(T38, void, T40)) → U12_gga(T38, T40, pB_in_ga(T38, T40))
U12_gga(T38, T40, pB_out_ga(T38, T40)) → deleteC_out_gga(T38, tree(T38, void, void), tree(T38, void, T40))
deleteC_in_gga(s(T50), tree(s(T50), void, void), tree(s(T50), T45, void)) → U13_gga(T50, T45, pD_in_ga(T50, T45))
pD_in_ga(T50, T45) → U4_ga(T50, T45, lessA_in_g(T50))
U4_ga(T50, T45, lessA_out_g(T50)) → pD_out_ga(T50, T45)
U4_ga(T50, T45, lessA_out_g(T50)) → U5_ga(T50, T45, deleteC_in_gga(s(T50), void, T45))
deleteC_in_gga(T57, tree(T57, void, void), tree(T57, void, T59)) → U14_gga(T57, T59, pB_in_ga(T57, T59))
U14_gga(T57, T59, pB_out_ga(T57, T59)) → deleteC_out_gga(T57, tree(T57, void, void), tree(T57, void, T59))
deleteC_in_gga(s(T67), tree(s(T67), void, void), tree(s(T67), void, T64)) → U15_gga(T67, T64, pD_in_ga(T67, T64))
U15_gga(T67, T64, pD_out_ga(T67, T64)) → deleteC_out_gga(s(T67), tree(s(T67), void, void), tree(s(T67), void, T64))
deleteC_in_gga(T72, tree(T72, void, tree(T86, void, T87)), tree(T86, void, T87)) → deleteC_out_gga(T72, tree(T72, void, tree(T86, void, T87)), tree(T86, void, T87))
deleteC_in_gga(T72, tree(T72, void, tree(T112, T113, T114)), tree(T118, void, tree(T112, T119, T117))) → U16_gga(T72, T112, T113, T114, T118, T119, T117, delminE_in_gaa(T113, T118, T119))
delminE_in_gaa(tree(T132, void, T133), T132, T133) → delminE_out_gaa(tree(T132, void, T133), T132, T133)
delminE_in_gaa(tree(T146, T147, T148), T152, tree(T146, T153, T151)) → U6_gaa(T146, T147, T148, T152, T153, T151, delminE_in_gaa(T147, T152, T153))
U6_gaa(T146, T147, T148, T152, T153, T151, delminE_out_gaa(T147, T152, T153)) → delminE_out_gaa(tree(T146, T147, T148), T152, tree(T146, T153, T151))
U16_gga(T72, T112, T113, T114, T118, T119, T117, delminE_out_gaa(T113, T118, T119)) → deleteC_out_gga(T72, tree(T72, void, tree(T112, T113, T114)), tree(T118, void, tree(T112, T119, T117)))
deleteC_in_gga(T170, tree(T170, void, T171), tree(T170, T173, T171)) → U17_gga(T170, T171, T173, pB_in_ga(T170, T173))
U17_gga(T170, T171, T173, pB_out_ga(T170, T173)) → deleteC_out_gga(T170, tree(T170, void, T171), tree(T170, T173, T171))
deleteC_in_gga(T180, tree(T180, void, T181), tree(T180, void, T183)) → U18_gga(T180, T181, T183, pF_in_gga(T180, T181, T183))
pF_in_gga(T180, T181, T183) → U7_gga(T180, T181, T183, lessA_in_g(T180))
U7_gga(T180, T181, T183, lessA_out_g(T180)) → pF_out_gga(T180, T181, T183)
U7_gga(T180, T181, T183, lessA_out_g(T180)) → U8_gga(T180, T181, T183, deleteC_in_gga(T180, T181, T183))
deleteC_in_gga(s(T199), tree(s(T199), void, T192), tree(s(T199), T194, T192)) → U19_gga(T199, T192, T194, lessA_in_g(T199))
U19_gga(T199, T192, T194, lessA_out_g(T199)) → deleteC_out_gga(s(T199), tree(s(T199), void, T192), tree(s(T199), T194, T192))
U19_gga(T199, T192, T194, lessA_out_g(T199)) → U20_gga(T199, T192, T194, deleteC_in_gga(s(T199), void, T194))
deleteC_in_gga(T208, tree(T208, void, T209), tree(T208, void, T211)) → U21_gga(T208, T209, T211, pF_in_gga(T208, T209, T211))
U21_gga(T208, T209, T211, pF_out_gga(T208, T209, T211)) → deleteC_out_gga(T208, tree(T208, void, T209), tree(T208, void, T211))
deleteC_in_gga(s(T221), tree(s(T221), void, T216), tree(s(T221), void, T218)) → U22_gga(T221, T216, T218, lessA_in_g(T221))
U22_gga(T221, T216, T218, lessA_out_g(T221)) → deleteC_out_gga(s(T221), tree(s(T221), void, T216), tree(s(T221), void, T218))
U22_gga(T221, T216, T218, lessA_out_g(T221)) → U23_gga(T221, T216, T218, deleteC_in_gga(s(T221), T216, T218))
deleteC_in_gga(T228, tree(T228, T229, void), T229) → deleteC_out_gga(T228, tree(T228, T229, void), T229)
deleteC_in_gga(T252, tree(T252, T253, void), tree(T252, T255, void)) → U24_gga(T252, T253, T255, lessA_in_g(T252))
U24_gga(T252, T253, T255, lessA_out_g(T252)) → deleteC_out_gga(T252, tree(T252, T253, void), tree(T252, T255, void))
U24_gga(T252, T253, T255, lessA_out_g(T252)) → U25_gga(T252, T253, T255, deleteC_in_gga(T252, T253, T255))
deleteC_in_gga(T266, tree(T266, T267, void), tree(T266, T267, T269)) → U26_gga(T266, T267, T269, pB_in_ga(T266, T269))
U26_gga(T266, T267, T269, pB_out_ga(T266, T269)) → deleteC_out_gga(T266, tree(T266, T267, void), tree(T266, T267, T269))
deleteC_in_gga(s(T281), tree(s(T281), T274, void), tree(s(T281), T276, void)) → U27_gga(T281, T274, T276, lessA_in_g(T281))
U27_gga(T281, T274, T276, lessA_out_g(T281)) → deleteC_out_gga(s(T281), tree(s(T281), T274, void), tree(s(T281), T276, void))
U27_gga(T281, T274, T276, lessA_out_g(T281)) → U28_gga(T281, T274, T276, deleteC_in_gga(s(T281), T274, T276))
deleteC_in_gga(T292, tree(T292, T293, void), tree(T292, T293, T295)) → U29_gga(T292, T293, T295, pB_in_ga(T292, T295))
U29_gga(T292, T293, T295, pB_out_ga(T292, T295)) → deleteC_out_gga(T292, tree(T292, T293, void), tree(T292, T293, T295))
deleteC_in_gga(s(T305), tree(s(T305), T300, void), tree(s(T305), T300, T302)) → U30_gga(T305, T300, T302, lessA_in_g(T305))
U30_gga(T305, T300, T302, lessA_out_g(T305)) → deleteC_out_gga(s(T305), tree(s(T305), T300, void), tree(s(T305), T300, T302))
U30_gga(T305, T300, T302, lessA_out_g(T305)) → U31_gga(T305, T300, T302, deleteC_in_gga(s(T305), void, T302))
deleteC_in_gga(T313, tree(T313, T314, tree(T328, void, T329)), tree(T328, T314, T329)) → deleteC_out_gga(T313, tree(T313, T314, tree(T328, void, T329)), tree(T328, T314, T329))
deleteC_in_gga(T313, tree(T313, T314, tree(T354, T355, T356)), tree(T360, T314, tree(T354, T361, T359))) → U32_gga(T313, T314, T354, T355, T356, T360, T361, T359, delminE_in_gaa(T355, T360, T361))
U32_gga(T313, T314, T354, T355, T356, T360, T361, T359, delminE_out_gaa(T355, T360, T361)) → deleteC_out_gga(T313, tree(T313, T314, tree(T354, T355, T356)), tree(T360, T314, tree(T354, T361, T359)))
deleteC_in_gga(T382, tree(T382, T383, T384), tree(T382, T386, T384)) → U33_gga(T382, T383, T384, T386, lessA_in_g(T382))
U33_gga(T382, T383, T384, T386, lessA_out_g(T382)) → deleteC_out_gga(T382, tree(T382, T383, T384), tree(T382, T386, T384))
U33_gga(T382, T383, T384, T386, lessA_out_g(T382)) → U34_gga(T382, T383, T384, T386, deleteC_in_gga(T382, T383, T386))
deleteC_in_gga(T399, tree(T399, T400, T401), tree(T399, T400, T403)) → U35_gga(T399, T400, T401, T403, lessA_in_g(T399))
U35_gga(T399, T400, T401, T403, lessA_out_g(T399)) → deleteC_out_gga(T399, tree(T399, T400, T401), tree(T399, T400, T403))
U35_gga(T399, T400, T401, T403, lessA_out_g(T399)) → U36_gga(T399, T400, T401, T403, deleteC_in_gga(T399, T401, T403))
deleteC_in_gga(0, tree(s(T423), T415, T416), tree(s(T423), T418, T416)) → U37_gga(T423, T415, T416, T418, deleteC_in_gga(0, T415, T418))
deleteC_in_gga(s(T434), tree(s(T435), T415, T416), tree(s(T435), T418, T416)) → U38_gga(T434, T435, T415, T416, T418, lessH_in_gg(T434, T435))
lessH_in_gg(0, s(T444)) → lessH_out_gg(0, s(T444))
lessH_in_gg(s(0), s(s(T457))) → lessH_out_gg(s(0), s(s(T457)))
lessH_in_gg(s(s(0)), s(s(s(T470)))) → lessH_out_gg(s(s(0)), s(s(s(T470))))
lessH_in_gg(s(s(s(0))), s(s(s(s(T483))))) → lessH_out_gg(s(s(s(0))), s(s(s(s(T483)))))
lessH_in_gg(s(s(s(s(0)))), s(s(s(s(s(T496)))))) → lessH_out_gg(s(s(s(s(0)))), s(s(s(s(s(T496))))))
lessH_in_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T509))))))) → lessH_out_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T509)))))))
lessH_in_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T522)))))))) → lessH_out_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T522))))))))
lessH_in_gg(s(s(s(s(s(s(s(T527))))))), s(s(s(s(s(s(s(T528)))))))) → U10_gg(T527, T528, lessG_in_gg(T527, T528))
lessG_in_gg(0, s(T539)) → lessG_out_gg(0, s(T539))
lessG_in_gg(s(T544), s(T545)) → U9_gg(T544, T545, lessG_in_gg(T544, T545))
U9_gg(T544, T545, lessG_out_gg(T544, T545)) → lessG_out_gg(s(T544), s(T545))
U10_gg(T527, T528, lessG_out_gg(T527, T528)) → lessH_out_gg(s(s(s(s(s(s(s(T527))))))), s(s(s(s(s(s(s(T528))))))))
U38_gga(T434, T435, T415, T416, T418, lessH_out_gg(T434, T435)) → deleteC_out_gga(s(T434), tree(s(T435), T415, T416), tree(s(T435), T418, T416))
U38_gga(T434, T435, T415, T416, T418, lessH_out_gg(T434, T435)) → U39_gga(T434, T435, T415, T416, T418, deleteC_in_gga(s(T434), T415, T418))
deleteC_in_gga(T562, tree(T563, T564, T565), tree(T563, T564, T567)) → U40_gga(T562, T563, T564, T565, T567, lessG_in_gg(T563, T562))
U40_gga(T562, T563, T564, T565, T567, lessG_out_gg(T563, T562)) → deleteC_out_gga(T562, tree(T563, T564, T565), tree(T563, T564, T567))
U40_gga(T562, T563, T564, T565, T567, lessG_out_gg(T563, T562)) → U41_gga(T562, T563, T564, T565, T567, deleteC_in_gga(T562, T565, T567))
deleteC_in_gga(s(T591), tree(0, T583, T584), tree(0, T583, T586)) → U42_gga(T591, T583, T584, T586, deleteC_in_gga(s(T591), T584, T586))
deleteC_in_gga(s(T601), tree(s(T600), T583, T584), tree(s(T600), T583, T586)) → U43_gga(T601, T600, T583, T584, T586, lessG_in_gg(T600, T601))
U43_gga(T601, T600, T583, T584, T586, lessG_out_gg(T600, T601)) → deleteC_out_gga(s(T601), tree(s(T600), T583, T584), tree(s(T600), T583, T586))
U43_gga(T601, T600, T583, T584, T586, lessG_out_gg(T600, T601)) → U44_gga(T601, T600, T583, T584, T586, deleteC_in_gga(s(T601), T584, T586))
U44_gga(T601, T600, T583, T584, T586, deleteC_out_gga(s(T601), T584, T586)) → deleteC_out_gga(s(T601), tree(s(T600), T583, T584), tree(s(T600), T583, T586))
U42_gga(T591, T583, T584, T586, deleteC_out_gga(s(T591), T584, T586)) → deleteC_out_gga(s(T591), tree(0, T583, T584), tree(0, T583, T586))
U41_gga(T562, T563, T564, T565, T567, deleteC_out_gga(T562, T565, T567)) → deleteC_out_gga(T562, tree(T563, T564, T565), tree(T563, T564, T567))
U39_gga(T434, T435, T415, T416, T418, deleteC_out_gga(s(T434), T415, T418)) → deleteC_out_gga(s(T434), tree(s(T435), T415, T416), tree(s(T435), T418, T416))
U37_gga(T423, T415, T416, T418, deleteC_out_gga(0, T415, T418)) → deleteC_out_gga(0, tree(s(T423), T415, T416), tree(s(T423), T418, T416))
U36_gga(T399, T400, T401, T403, deleteC_out_gga(T399, T401, T403)) → deleteC_out_gga(T399, tree(T399, T400, T401), tree(T399, T400, T403))
U34_gga(T382, T383, T384, T386, deleteC_out_gga(T382, T383, T386)) → deleteC_out_gga(T382, tree(T382, T383, T384), tree(T382, T386, T384))
U31_gga(T305, T300, T302, deleteC_out_gga(s(T305), void, T302)) → deleteC_out_gga(s(T305), tree(s(T305), T300, void), tree(s(T305), T300, T302))
U28_gga(T281, T274, T276, deleteC_out_gga(s(T281), T274, T276)) → deleteC_out_gga(s(T281), tree(s(T281), T274, void), tree(s(T281), T276, void))
U25_gga(T252, T253, T255, deleteC_out_gga(T252, T253, T255)) → deleteC_out_gga(T252, tree(T252, T253, void), tree(T252, T255, void))
U23_gga(T221, T216, T218, deleteC_out_gga(s(T221), T216, T218)) → deleteC_out_gga(s(T221), tree(s(T221), void, T216), tree(s(T221), void, T218))
U20_gga(T199, T192, T194, deleteC_out_gga(s(T199), void, T194)) → deleteC_out_gga(s(T199), tree(s(T199), void, T192), tree(s(T199), T194, T192))
U8_gga(T180, T181, T183, deleteC_out_gga(T180, T181, T183)) → pF_out_gga(T180, T181, T183)
U18_gga(T180, T181, T183, pF_out_gga(T180, T181, T183)) → deleteC_out_gga(T180, tree(T180, void, T181), tree(T180, void, T183))
U5_ga(T50, T45, deleteC_out_gga(s(T50), void, T45)) → pD_out_ga(T50, T45)
U13_gga(T50, T45, pD_out_ga(T50, T45)) → deleteC_out_gga(s(T50), tree(s(T50), void, void), tree(s(T50), T45, void))
U3_ga(T26, T28, deleteC_out_gga(T26, void, T28)) → pB_out_ga(T26, T28)
U11_gga(T26, T28, pB_out_ga(T26, T28)) → deleteC_out_gga(T26, tree(T26, void, void), tree(T26, T28, void))

The argument filtering Pi contains the following mapping:
deleteC_in_gga(x1, x2, x3)  =  deleteC_in_gga(x1, x2)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
void  =  void
deleteC_out_gga(x1, x2, x3)  =  deleteC_out_gga
U11_gga(x1, x2, x3)  =  U11_gga(x3)
pB_in_ga(x1, x2)  =  pB_in_ga(x1)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
lessA_in_g(x1)  =  lessA_in_g(x1)
s(x1)  =  s(x1)
U1_g(x1, x2)  =  U1_g(x2)
lessA_out_g(x1)  =  lessA_out_g
pB_out_ga(x1, x2)  =  pB_out_ga
U3_ga(x1, x2, x3)  =  U3_ga(x3)
U12_gga(x1, x2, x3)  =  U12_gga(x3)
U13_gga(x1, x2, x3)  =  U13_gga(x3)
pD_in_ga(x1, x2)  =  pD_in_ga(x1)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
pD_out_ga(x1, x2)  =  pD_out_ga
U5_ga(x1, x2, x3)  =  U5_ga(x3)
U14_gga(x1, x2, x3)  =  U14_gga(x3)
U15_gga(x1, x2, x3)  =  U15_gga(x3)
U16_gga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U16_gga(x8)
delminE_in_gaa(x1, x2, x3)  =  delminE_in_gaa(x1)
delminE_out_gaa(x1, x2, x3)  =  delminE_out_gaa(x2)
U6_gaa(x1, x2, x3, x4, x5, x6, x7)  =  U6_gaa(x7)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x4)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x4)
pF_in_gga(x1, x2, x3)  =  pF_in_gga(x1, x2)
U7_gga(x1, x2, x3, x4)  =  U7_gga(x1, x2, x4)
pF_out_gga(x1, x2, x3)  =  pF_out_gga
U8_gga(x1, x2, x3, x4)  =  U8_gga(x4)
U19_gga(x1, x2, x3, x4)  =  U19_gga(x1, x4)
U20_gga(x1, x2, x3, x4)  =  U20_gga(x4)
U21_gga(x1, x2, x3, x4)  =  U21_gga(x4)
U22_gga(x1, x2, x3, x4)  =  U22_gga(x1, x2, x4)
U23_gga(x1, x2, x3, x4)  =  U23_gga(x4)
U24_gga(x1, x2, x3, x4)  =  U24_gga(x1, x2, x4)
U25_gga(x1, x2, x3, x4)  =  U25_gga(x4)
U26_gga(x1, x2, x3, x4)  =  U26_gga(x4)
U27_gga(x1, x2, x3, x4)  =  U27_gga(x1, x2, x4)
U28_gga(x1, x2, x3, x4)  =  U28_gga(x4)
U29_gga(x1, x2, x3, x4)  =  U29_gga(x4)
U30_gga(x1, x2, x3, x4)  =  U30_gga(x1, x4)
U31_gga(x1, x2, x3, x4)  =  U31_gga(x4)
U32_gga(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U32_gga(x9)
U33_gga(x1, x2, x3, x4, x5)  =  U33_gga(x1, x2, x5)
U34_gga(x1, x2, x3, x4, x5)  =  U34_gga(x5)
U35_gga(x1, x2, x3, x4, x5)  =  U35_gga(x1, x3, x5)
U36_gga(x1, x2, x3, x4, x5)  =  U36_gga(x5)
0  =  0
U37_gga(x1, x2, x3, x4, x5)  =  U37_gga(x5)
U38_gga(x1, x2, x3, x4, x5, x6)  =  U38_gga(x1, x3, x6)
lessH_in_gg(x1, x2)  =  lessH_in_gg(x1, x2)
lessH_out_gg(x1, x2)  =  lessH_out_gg
U10_gg(x1, x2, x3)  =  U10_gg(x3)
lessG_in_gg(x1, x2)  =  lessG_in_gg(x1, x2)
lessG_out_gg(x1, x2)  =  lessG_out_gg
U9_gg(x1, x2, x3)  =  U9_gg(x3)
U39_gga(x1, x2, x3, x4, x5, x6)  =  U39_gga(x6)
U40_gga(x1, x2, x3, x4, x5, x6)  =  U40_gga(x1, x4, x6)
U41_gga(x1, x2, x3, x4, x5, x6)  =  U41_gga(x6)
U42_gga(x1, x2, x3, x4, x5)  =  U42_gga(x5)
U43_gga(x1, x2, x3, x4, x5, x6)  =  U43_gga(x1, x4, x6)
U44_gga(x1, x2, x3, x4, x5, x6)  =  U44_gga(x6)
LESSG_IN_GG(x1, x2)  =  LESSG_IN_GG(x1, x2)

We have to consider all (P,R,Pi)-chains

(10) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(11) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

LESSG_IN_GG(s(T544), s(T545)) → LESSG_IN_GG(T544, T545)

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains

(12) PiDPToQDPProof (EQUIVALENT transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(13) Obligation:

Q DP problem:
The TRS P consists of the following rules:

LESSG_IN_GG(s(T544), s(T545)) → LESSG_IN_GG(T544, T545)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(14) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • LESSG_IN_GG(s(T544), s(T545)) → LESSG_IN_GG(T544, T545)
    The graph contains the following edges 1 > 1, 2 > 2

(15) YES

(16) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

DELMINE_IN_GAA(tree(T146, T147, T148), T152, tree(T146, T153, T151)) → DELMINE_IN_GAA(T147, T152, T153)

The TRS R consists of the following rules:

deleteC_in_gga(T6, tree(T6, void, T7), T7) → deleteC_out_gga(T6, tree(T6, void, T7), T7)
deleteC_in_gga(T9, tree(T9, void, void), void) → deleteC_out_gga(T9, tree(T9, void, void), void)
deleteC_in_gga(T26, tree(T26, void, void), tree(T26, T28, void)) → U11_gga(T26, T28, pB_in_ga(T26, T28))
pB_in_ga(T26, T28) → U2_ga(T26, T28, lessA_in_g(T26))
lessA_in_g(s(T31)) → U1_g(T31, lessA_in_g(T31))
U1_g(T31, lessA_out_g(T31)) → lessA_out_g(s(T31))
U2_ga(T26, T28, lessA_out_g(T26)) → pB_out_ga(T26, T28)
U2_ga(T26, T28, lessA_out_g(T26)) → U3_ga(T26, T28, deleteC_in_gga(T26, void, T28))
deleteC_in_gga(T38, tree(T38, void, void), tree(T38, void, T40)) → U12_gga(T38, T40, pB_in_ga(T38, T40))
U12_gga(T38, T40, pB_out_ga(T38, T40)) → deleteC_out_gga(T38, tree(T38, void, void), tree(T38, void, T40))
deleteC_in_gga(s(T50), tree(s(T50), void, void), tree(s(T50), T45, void)) → U13_gga(T50, T45, pD_in_ga(T50, T45))
pD_in_ga(T50, T45) → U4_ga(T50, T45, lessA_in_g(T50))
U4_ga(T50, T45, lessA_out_g(T50)) → pD_out_ga(T50, T45)
U4_ga(T50, T45, lessA_out_g(T50)) → U5_ga(T50, T45, deleteC_in_gga(s(T50), void, T45))
deleteC_in_gga(T57, tree(T57, void, void), tree(T57, void, T59)) → U14_gga(T57, T59, pB_in_ga(T57, T59))
U14_gga(T57, T59, pB_out_ga(T57, T59)) → deleteC_out_gga(T57, tree(T57, void, void), tree(T57, void, T59))
deleteC_in_gga(s(T67), tree(s(T67), void, void), tree(s(T67), void, T64)) → U15_gga(T67, T64, pD_in_ga(T67, T64))
U15_gga(T67, T64, pD_out_ga(T67, T64)) → deleteC_out_gga(s(T67), tree(s(T67), void, void), tree(s(T67), void, T64))
deleteC_in_gga(T72, tree(T72, void, tree(T86, void, T87)), tree(T86, void, T87)) → deleteC_out_gga(T72, tree(T72, void, tree(T86, void, T87)), tree(T86, void, T87))
deleteC_in_gga(T72, tree(T72, void, tree(T112, T113, T114)), tree(T118, void, tree(T112, T119, T117))) → U16_gga(T72, T112, T113, T114, T118, T119, T117, delminE_in_gaa(T113, T118, T119))
delminE_in_gaa(tree(T132, void, T133), T132, T133) → delminE_out_gaa(tree(T132, void, T133), T132, T133)
delminE_in_gaa(tree(T146, T147, T148), T152, tree(T146, T153, T151)) → U6_gaa(T146, T147, T148, T152, T153, T151, delminE_in_gaa(T147, T152, T153))
U6_gaa(T146, T147, T148, T152, T153, T151, delminE_out_gaa(T147, T152, T153)) → delminE_out_gaa(tree(T146, T147, T148), T152, tree(T146, T153, T151))
U16_gga(T72, T112, T113, T114, T118, T119, T117, delminE_out_gaa(T113, T118, T119)) → deleteC_out_gga(T72, tree(T72, void, tree(T112, T113, T114)), tree(T118, void, tree(T112, T119, T117)))
deleteC_in_gga(T170, tree(T170, void, T171), tree(T170, T173, T171)) → U17_gga(T170, T171, T173, pB_in_ga(T170, T173))
U17_gga(T170, T171, T173, pB_out_ga(T170, T173)) → deleteC_out_gga(T170, tree(T170, void, T171), tree(T170, T173, T171))
deleteC_in_gga(T180, tree(T180, void, T181), tree(T180, void, T183)) → U18_gga(T180, T181, T183, pF_in_gga(T180, T181, T183))
pF_in_gga(T180, T181, T183) → U7_gga(T180, T181, T183, lessA_in_g(T180))
U7_gga(T180, T181, T183, lessA_out_g(T180)) → pF_out_gga(T180, T181, T183)
U7_gga(T180, T181, T183, lessA_out_g(T180)) → U8_gga(T180, T181, T183, deleteC_in_gga(T180, T181, T183))
deleteC_in_gga(s(T199), tree(s(T199), void, T192), tree(s(T199), T194, T192)) → U19_gga(T199, T192, T194, lessA_in_g(T199))
U19_gga(T199, T192, T194, lessA_out_g(T199)) → deleteC_out_gga(s(T199), tree(s(T199), void, T192), tree(s(T199), T194, T192))
U19_gga(T199, T192, T194, lessA_out_g(T199)) → U20_gga(T199, T192, T194, deleteC_in_gga(s(T199), void, T194))
deleteC_in_gga(T208, tree(T208, void, T209), tree(T208, void, T211)) → U21_gga(T208, T209, T211, pF_in_gga(T208, T209, T211))
U21_gga(T208, T209, T211, pF_out_gga(T208, T209, T211)) → deleteC_out_gga(T208, tree(T208, void, T209), tree(T208, void, T211))
deleteC_in_gga(s(T221), tree(s(T221), void, T216), tree(s(T221), void, T218)) → U22_gga(T221, T216, T218, lessA_in_g(T221))
U22_gga(T221, T216, T218, lessA_out_g(T221)) → deleteC_out_gga(s(T221), tree(s(T221), void, T216), tree(s(T221), void, T218))
U22_gga(T221, T216, T218, lessA_out_g(T221)) → U23_gga(T221, T216, T218, deleteC_in_gga(s(T221), T216, T218))
deleteC_in_gga(T228, tree(T228, T229, void), T229) → deleteC_out_gga(T228, tree(T228, T229, void), T229)
deleteC_in_gga(T252, tree(T252, T253, void), tree(T252, T255, void)) → U24_gga(T252, T253, T255, lessA_in_g(T252))
U24_gga(T252, T253, T255, lessA_out_g(T252)) → deleteC_out_gga(T252, tree(T252, T253, void), tree(T252, T255, void))
U24_gga(T252, T253, T255, lessA_out_g(T252)) → U25_gga(T252, T253, T255, deleteC_in_gga(T252, T253, T255))
deleteC_in_gga(T266, tree(T266, T267, void), tree(T266, T267, T269)) → U26_gga(T266, T267, T269, pB_in_ga(T266, T269))
U26_gga(T266, T267, T269, pB_out_ga(T266, T269)) → deleteC_out_gga(T266, tree(T266, T267, void), tree(T266, T267, T269))
deleteC_in_gga(s(T281), tree(s(T281), T274, void), tree(s(T281), T276, void)) → U27_gga(T281, T274, T276, lessA_in_g(T281))
U27_gga(T281, T274, T276, lessA_out_g(T281)) → deleteC_out_gga(s(T281), tree(s(T281), T274, void), tree(s(T281), T276, void))
U27_gga(T281, T274, T276, lessA_out_g(T281)) → U28_gga(T281, T274, T276, deleteC_in_gga(s(T281), T274, T276))
deleteC_in_gga(T292, tree(T292, T293, void), tree(T292, T293, T295)) → U29_gga(T292, T293, T295, pB_in_ga(T292, T295))
U29_gga(T292, T293, T295, pB_out_ga(T292, T295)) → deleteC_out_gga(T292, tree(T292, T293, void), tree(T292, T293, T295))
deleteC_in_gga(s(T305), tree(s(T305), T300, void), tree(s(T305), T300, T302)) → U30_gga(T305, T300, T302, lessA_in_g(T305))
U30_gga(T305, T300, T302, lessA_out_g(T305)) → deleteC_out_gga(s(T305), tree(s(T305), T300, void), tree(s(T305), T300, T302))
U30_gga(T305, T300, T302, lessA_out_g(T305)) → U31_gga(T305, T300, T302, deleteC_in_gga(s(T305), void, T302))
deleteC_in_gga(T313, tree(T313, T314, tree(T328, void, T329)), tree(T328, T314, T329)) → deleteC_out_gga(T313, tree(T313, T314, tree(T328, void, T329)), tree(T328, T314, T329))
deleteC_in_gga(T313, tree(T313, T314, tree(T354, T355, T356)), tree(T360, T314, tree(T354, T361, T359))) → U32_gga(T313, T314, T354, T355, T356, T360, T361, T359, delminE_in_gaa(T355, T360, T361))
U32_gga(T313, T314, T354, T355, T356, T360, T361, T359, delminE_out_gaa(T355, T360, T361)) → deleteC_out_gga(T313, tree(T313, T314, tree(T354, T355, T356)), tree(T360, T314, tree(T354, T361, T359)))
deleteC_in_gga(T382, tree(T382, T383, T384), tree(T382, T386, T384)) → U33_gga(T382, T383, T384, T386, lessA_in_g(T382))
U33_gga(T382, T383, T384, T386, lessA_out_g(T382)) → deleteC_out_gga(T382, tree(T382, T383, T384), tree(T382, T386, T384))
U33_gga(T382, T383, T384, T386, lessA_out_g(T382)) → U34_gga(T382, T383, T384, T386, deleteC_in_gga(T382, T383, T386))
deleteC_in_gga(T399, tree(T399, T400, T401), tree(T399, T400, T403)) → U35_gga(T399, T400, T401, T403, lessA_in_g(T399))
U35_gga(T399, T400, T401, T403, lessA_out_g(T399)) → deleteC_out_gga(T399, tree(T399, T400, T401), tree(T399, T400, T403))
U35_gga(T399, T400, T401, T403, lessA_out_g(T399)) → U36_gga(T399, T400, T401, T403, deleteC_in_gga(T399, T401, T403))
deleteC_in_gga(0, tree(s(T423), T415, T416), tree(s(T423), T418, T416)) → U37_gga(T423, T415, T416, T418, deleteC_in_gga(0, T415, T418))
deleteC_in_gga(s(T434), tree(s(T435), T415, T416), tree(s(T435), T418, T416)) → U38_gga(T434, T435, T415, T416, T418, lessH_in_gg(T434, T435))
lessH_in_gg(0, s(T444)) → lessH_out_gg(0, s(T444))
lessH_in_gg(s(0), s(s(T457))) → lessH_out_gg(s(0), s(s(T457)))
lessH_in_gg(s(s(0)), s(s(s(T470)))) → lessH_out_gg(s(s(0)), s(s(s(T470))))
lessH_in_gg(s(s(s(0))), s(s(s(s(T483))))) → lessH_out_gg(s(s(s(0))), s(s(s(s(T483)))))
lessH_in_gg(s(s(s(s(0)))), s(s(s(s(s(T496)))))) → lessH_out_gg(s(s(s(s(0)))), s(s(s(s(s(T496))))))
lessH_in_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T509))))))) → lessH_out_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T509)))))))
lessH_in_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T522)))))))) → lessH_out_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T522))))))))
lessH_in_gg(s(s(s(s(s(s(s(T527))))))), s(s(s(s(s(s(s(T528)))))))) → U10_gg(T527, T528, lessG_in_gg(T527, T528))
lessG_in_gg(0, s(T539)) → lessG_out_gg(0, s(T539))
lessG_in_gg(s(T544), s(T545)) → U9_gg(T544, T545, lessG_in_gg(T544, T545))
U9_gg(T544, T545, lessG_out_gg(T544, T545)) → lessG_out_gg(s(T544), s(T545))
U10_gg(T527, T528, lessG_out_gg(T527, T528)) → lessH_out_gg(s(s(s(s(s(s(s(T527))))))), s(s(s(s(s(s(s(T528))))))))
U38_gga(T434, T435, T415, T416, T418, lessH_out_gg(T434, T435)) → deleteC_out_gga(s(T434), tree(s(T435), T415, T416), tree(s(T435), T418, T416))
U38_gga(T434, T435, T415, T416, T418, lessH_out_gg(T434, T435)) → U39_gga(T434, T435, T415, T416, T418, deleteC_in_gga(s(T434), T415, T418))
deleteC_in_gga(T562, tree(T563, T564, T565), tree(T563, T564, T567)) → U40_gga(T562, T563, T564, T565, T567, lessG_in_gg(T563, T562))
U40_gga(T562, T563, T564, T565, T567, lessG_out_gg(T563, T562)) → deleteC_out_gga(T562, tree(T563, T564, T565), tree(T563, T564, T567))
U40_gga(T562, T563, T564, T565, T567, lessG_out_gg(T563, T562)) → U41_gga(T562, T563, T564, T565, T567, deleteC_in_gga(T562, T565, T567))
deleteC_in_gga(s(T591), tree(0, T583, T584), tree(0, T583, T586)) → U42_gga(T591, T583, T584, T586, deleteC_in_gga(s(T591), T584, T586))
deleteC_in_gga(s(T601), tree(s(T600), T583, T584), tree(s(T600), T583, T586)) → U43_gga(T601, T600, T583, T584, T586, lessG_in_gg(T600, T601))
U43_gga(T601, T600, T583, T584, T586, lessG_out_gg(T600, T601)) → deleteC_out_gga(s(T601), tree(s(T600), T583, T584), tree(s(T600), T583, T586))
U43_gga(T601, T600, T583, T584, T586, lessG_out_gg(T600, T601)) → U44_gga(T601, T600, T583, T584, T586, deleteC_in_gga(s(T601), T584, T586))
U44_gga(T601, T600, T583, T584, T586, deleteC_out_gga(s(T601), T584, T586)) → deleteC_out_gga(s(T601), tree(s(T600), T583, T584), tree(s(T600), T583, T586))
U42_gga(T591, T583, T584, T586, deleteC_out_gga(s(T591), T584, T586)) → deleteC_out_gga(s(T591), tree(0, T583, T584), tree(0, T583, T586))
U41_gga(T562, T563, T564, T565, T567, deleteC_out_gga(T562, T565, T567)) → deleteC_out_gga(T562, tree(T563, T564, T565), tree(T563, T564, T567))
U39_gga(T434, T435, T415, T416, T418, deleteC_out_gga(s(T434), T415, T418)) → deleteC_out_gga(s(T434), tree(s(T435), T415, T416), tree(s(T435), T418, T416))
U37_gga(T423, T415, T416, T418, deleteC_out_gga(0, T415, T418)) → deleteC_out_gga(0, tree(s(T423), T415, T416), tree(s(T423), T418, T416))
U36_gga(T399, T400, T401, T403, deleteC_out_gga(T399, T401, T403)) → deleteC_out_gga(T399, tree(T399, T400, T401), tree(T399, T400, T403))
U34_gga(T382, T383, T384, T386, deleteC_out_gga(T382, T383, T386)) → deleteC_out_gga(T382, tree(T382, T383, T384), tree(T382, T386, T384))
U31_gga(T305, T300, T302, deleteC_out_gga(s(T305), void, T302)) → deleteC_out_gga(s(T305), tree(s(T305), T300, void), tree(s(T305), T300, T302))
U28_gga(T281, T274, T276, deleteC_out_gga(s(T281), T274, T276)) → deleteC_out_gga(s(T281), tree(s(T281), T274, void), tree(s(T281), T276, void))
U25_gga(T252, T253, T255, deleteC_out_gga(T252, T253, T255)) → deleteC_out_gga(T252, tree(T252, T253, void), tree(T252, T255, void))
U23_gga(T221, T216, T218, deleteC_out_gga(s(T221), T216, T218)) → deleteC_out_gga(s(T221), tree(s(T221), void, T216), tree(s(T221), void, T218))
U20_gga(T199, T192, T194, deleteC_out_gga(s(T199), void, T194)) → deleteC_out_gga(s(T199), tree(s(T199), void, T192), tree(s(T199), T194, T192))
U8_gga(T180, T181, T183, deleteC_out_gga(T180, T181, T183)) → pF_out_gga(T180, T181, T183)
U18_gga(T180, T181, T183, pF_out_gga(T180, T181, T183)) → deleteC_out_gga(T180, tree(T180, void, T181), tree(T180, void, T183))
U5_ga(T50, T45, deleteC_out_gga(s(T50), void, T45)) → pD_out_ga(T50, T45)
U13_gga(T50, T45, pD_out_ga(T50, T45)) → deleteC_out_gga(s(T50), tree(s(T50), void, void), tree(s(T50), T45, void))
U3_ga(T26, T28, deleteC_out_gga(T26, void, T28)) → pB_out_ga(T26, T28)
U11_gga(T26, T28, pB_out_ga(T26, T28)) → deleteC_out_gga(T26, tree(T26, void, void), tree(T26, T28, void))

The argument filtering Pi contains the following mapping:
deleteC_in_gga(x1, x2, x3)  =  deleteC_in_gga(x1, x2)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
void  =  void
deleteC_out_gga(x1, x2, x3)  =  deleteC_out_gga
U11_gga(x1, x2, x3)  =  U11_gga(x3)
pB_in_ga(x1, x2)  =  pB_in_ga(x1)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
lessA_in_g(x1)  =  lessA_in_g(x1)
s(x1)  =  s(x1)
U1_g(x1, x2)  =  U1_g(x2)
lessA_out_g(x1)  =  lessA_out_g
pB_out_ga(x1, x2)  =  pB_out_ga
U3_ga(x1, x2, x3)  =  U3_ga(x3)
U12_gga(x1, x2, x3)  =  U12_gga(x3)
U13_gga(x1, x2, x3)  =  U13_gga(x3)
pD_in_ga(x1, x2)  =  pD_in_ga(x1)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
pD_out_ga(x1, x2)  =  pD_out_ga
U5_ga(x1, x2, x3)  =  U5_ga(x3)
U14_gga(x1, x2, x3)  =  U14_gga(x3)
U15_gga(x1, x2, x3)  =  U15_gga(x3)
U16_gga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U16_gga(x8)
delminE_in_gaa(x1, x2, x3)  =  delminE_in_gaa(x1)
delminE_out_gaa(x1, x2, x3)  =  delminE_out_gaa(x2)
U6_gaa(x1, x2, x3, x4, x5, x6, x7)  =  U6_gaa(x7)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x4)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x4)
pF_in_gga(x1, x2, x3)  =  pF_in_gga(x1, x2)
U7_gga(x1, x2, x3, x4)  =  U7_gga(x1, x2, x4)
pF_out_gga(x1, x2, x3)  =  pF_out_gga
U8_gga(x1, x2, x3, x4)  =  U8_gga(x4)
U19_gga(x1, x2, x3, x4)  =  U19_gga(x1, x4)
U20_gga(x1, x2, x3, x4)  =  U20_gga(x4)
U21_gga(x1, x2, x3, x4)  =  U21_gga(x4)
U22_gga(x1, x2, x3, x4)  =  U22_gga(x1, x2, x4)
U23_gga(x1, x2, x3, x4)  =  U23_gga(x4)
U24_gga(x1, x2, x3, x4)  =  U24_gga(x1, x2, x4)
U25_gga(x1, x2, x3, x4)  =  U25_gga(x4)
U26_gga(x1, x2, x3, x4)  =  U26_gga(x4)
U27_gga(x1, x2, x3, x4)  =  U27_gga(x1, x2, x4)
U28_gga(x1, x2, x3, x4)  =  U28_gga(x4)
U29_gga(x1, x2, x3, x4)  =  U29_gga(x4)
U30_gga(x1, x2, x3, x4)  =  U30_gga(x1, x4)
U31_gga(x1, x2, x3, x4)  =  U31_gga(x4)
U32_gga(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U32_gga(x9)
U33_gga(x1, x2, x3, x4, x5)  =  U33_gga(x1, x2, x5)
U34_gga(x1, x2, x3, x4, x5)  =  U34_gga(x5)
U35_gga(x1, x2, x3, x4, x5)  =  U35_gga(x1, x3, x5)
U36_gga(x1, x2, x3, x4, x5)  =  U36_gga(x5)
0  =  0
U37_gga(x1, x2, x3, x4, x5)  =  U37_gga(x5)
U38_gga(x1, x2, x3, x4, x5, x6)  =  U38_gga(x1, x3, x6)
lessH_in_gg(x1, x2)  =  lessH_in_gg(x1, x2)
lessH_out_gg(x1, x2)  =  lessH_out_gg
U10_gg(x1, x2, x3)  =  U10_gg(x3)
lessG_in_gg(x1, x2)  =  lessG_in_gg(x1, x2)
lessG_out_gg(x1, x2)  =  lessG_out_gg
U9_gg(x1, x2, x3)  =  U9_gg(x3)
U39_gga(x1, x2, x3, x4, x5, x6)  =  U39_gga(x6)
U40_gga(x1, x2, x3, x4, x5, x6)  =  U40_gga(x1, x4, x6)
U41_gga(x1, x2, x3, x4, x5, x6)  =  U41_gga(x6)
U42_gga(x1, x2, x3, x4, x5)  =  U42_gga(x5)
U43_gga(x1, x2, x3, x4, x5, x6)  =  U43_gga(x1, x4, x6)
U44_gga(x1, x2, x3, x4, x5, x6)  =  U44_gga(x6)
DELMINE_IN_GAA(x1, x2, x3)  =  DELMINE_IN_GAA(x1)

We have to consider all (P,R,Pi)-chains

(17) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(18) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

DELMINE_IN_GAA(tree(T146, T147, T148), T152, tree(T146, T153, T151)) → DELMINE_IN_GAA(T147, T152, T153)

R is empty.
The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
DELMINE_IN_GAA(x1, x2, x3)  =  DELMINE_IN_GAA(x1)

We have to consider all (P,R,Pi)-chains

(19) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(20) Obligation:

Q DP problem:
The TRS P consists of the following rules:

DELMINE_IN_GAA(tree(T146, T147, T148)) → DELMINE_IN_GAA(T147)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(21) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • DELMINE_IN_GAA(tree(T146, T147, T148)) → DELMINE_IN_GAA(T147)
    The graph contains the following edges 1 > 1

(22) YES

(23) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

LESSA_IN_G(s(T31)) → LESSA_IN_G(T31)

The TRS R consists of the following rules:

deleteC_in_gga(T6, tree(T6, void, T7), T7) → deleteC_out_gga(T6, tree(T6, void, T7), T7)
deleteC_in_gga(T9, tree(T9, void, void), void) → deleteC_out_gga(T9, tree(T9, void, void), void)
deleteC_in_gga(T26, tree(T26, void, void), tree(T26, T28, void)) → U11_gga(T26, T28, pB_in_ga(T26, T28))
pB_in_ga(T26, T28) → U2_ga(T26, T28, lessA_in_g(T26))
lessA_in_g(s(T31)) → U1_g(T31, lessA_in_g(T31))
U1_g(T31, lessA_out_g(T31)) → lessA_out_g(s(T31))
U2_ga(T26, T28, lessA_out_g(T26)) → pB_out_ga(T26, T28)
U2_ga(T26, T28, lessA_out_g(T26)) → U3_ga(T26, T28, deleteC_in_gga(T26, void, T28))
deleteC_in_gga(T38, tree(T38, void, void), tree(T38, void, T40)) → U12_gga(T38, T40, pB_in_ga(T38, T40))
U12_gga(T38, T40, pB_out_ga(T38, T40)) → deleteC_out_gga(T38, tree(T38, void, void), tree(T38, void, T40))
deleteC_in_gga(s(T50), tree(s(T50), void, void), tree(s(T50), T45, void)) → U13_gga(T50, T45, pD_in_ga(T50, T45))
pD_in_ga(T50, T45) → U4_ga(T50, T45, lessA_in_g(T50))
U4_ga(T50, T45, lessA_out_g(T50)) → pD_out_ga(T50, T45)
U4_ga(T50, T45, lessA_out_g(T50)) → U5_ga(T50, T45, deleteC_in_gga(s(T50), void, T45))
deleteC_in_gga(T57, tree(T57, void, void), tree(T57, void, T59)) → U14_gga(T57, T59, pB_in_ga(T57, T59))
U14_gga(T57, T59, pB_out_ga(T57, T59)) → deleteC_out_gga(T57, tree(T57, void, void), tree(T57, void, T59))
deleteC_in_gga(s(T67), tree(s(T67), void, void), tree(s(T67), void, T64)) → U15_gga(T67, T64, pD_in_ga(T67, T64))
U15_gga(T67, T64, pD_out_ga(T67, T64)) → deleteC_out_gga(s(T67), tree(s(T67), void, void), tree(s(T67), void, T64))
deleteC_in_gga(T72, tree(T72, void, tree(T86, void, T87)), tree(T86, void, T87)) → deleteC_out_gga(T72, tree(T72, void, tree(T86, void, T87)), tree(T86, void, T87))
deleteC_in_gga(T72, tree(T72, void, tree(T112, T113, T114)), tree(T118, void, tree(T112, T119, T117))) → U16_gga(T72, T112, T113, T114, T118, T119, T117, delminE_in_gaa(T113, T118, T119))
delminE_in_gaa(tree(T132, void, T133), T132, T133) → delminE_out_gaa(tree(T132, void, T133), T132, T133)
delminE_in_gaa(tree(T146, T147, T148), T152, tree(T146, T153, T151)) → U6_gaa(T146, T147, T148, T152, T153, T151, delminE_in_gaa(T147, T152, T153))
U6_gaa(T146, T147, T148, T152, T153, T151, delminE_out_gaa(T147, T152, T153)) → delminE_out_gaa(tree(T146, T147, T148), T152, tree(T146, T153, T151))
U16_gga(T72, T112, T113, T114, T118, T119, T117, delminE_out_gaa(T113, T118, T119)) → deleteC_out_gga(T72, tree(T72, void, tree(T112, T113, T114)), tree(T118, void, tree(T112, T119, T117)))
deleteC_in_gga(T170, tree(T170, void, T171), tree(T170, T173, T171)) → U17_gga(T170, T171, T173, pB_in_ga(T170, T173))
U17_gga(T170, T171, T173, pB_out_ga(T170, T173)) → deleteC_out_gga(T170, tree(T170, void, T171), tree(T170, T173, T171))
deleteC_in_gga(T180, tree(T180, void, T181), tree(T180, void, T183)) → U18_gga(T180, T181, T183, pF_in_gga(T180, T181, T183))
pF_in_gga(T180, T181, T183) → U7_gga(T180, T181, T183, lessA_in_g(T180))
U7_gga(T180, T181, T183, lessA_out_g(T180)) → pF_out_gga(T180, T181, T183)
U7_gga(T180, T181, T183, lessA_out_g(T180)) → U8_gga(T180, T181, T183, deleteC_in_gga(T180, T181, T183))
deleteC_in_gga(s(T199), tree(s(T199), void, T192), tree(s(T199), T194, T192)) → U19_gga(T199, T192, T194, lessA_in_g(T199))
U19_gga(T199, T192, T194, lessA_out_g(T199)) → deleteC_out_gga(s(T199), tree(s(T199), void, T192), tree(s(T199), T194, T192))
U19_gga(T199, T192, T194, lessA_out_g(T199)) → U20_gga(T199, T192, T194, deleteC_in_gga(s(T199), void, T194))
deleteC_in_gga(T208, tree(T208, void, T209), tree(T208, void, T211)) → U21_gga(T208, T209, T211, pF_in_gga(T208, T209, T211))
U21_gga(T208, T209, T211, pF_out_gga(T208, T209, T211)) → deleteC_out_gga(T208, tree(T208, void, T209), tree(T208, void, T211))
deleteC_in_gga(s(T221), tree(s(T221), void, T216), tree(s(T221), void, T218)) → U22_gga(T221, T216, T218, lessA_in_g(T221))
U22_gga(T221, T216, T218, lessA_out_g(T221)) → deleteC_out_gga(s(T221), tree(s(T221), void, T216), tree(s(T221), void, T218))
U22_gga(T221, T216, T218, lessA_out_g(T221)) → U23_gga(T221, T216, T218, deleteC_in_gga(s(T221), T216, T218))
deleteC_in_gga(T228, tree(T228, T229, void), T229) → deleteC_out_gga(T228, tree(T228, T229, void), T229)
deleteC_in_gga(T252, tree(T252, T253, void), tree(T252, T255, void)) → U24_gga(T252, T253, T255, lessA_in_g(T252))
U24_gga(T252, T253, T255, lessA_out_g(T252)) → deleteC_out_gga(T252, tree(T252, T253, void), tree(T252, T255, void))
U24_gga(T252, T253, T255, lessA_out_g(T252)) → U25_gga(T252, T253, T255, deleteC_in_gga(T252, T253, T255))
deleteC_in_gga(T266, tree(T266, T267, void), tree(T266, T267, T269)) → U26_gga(T266, T267, T269, pB_in_ga(T266, T269))
U26_gga(T266, T267, T269, pB_out_ga(T266, T269)) → deleteC_out_gga(T266, tree(T266, T267, void), tree(T266, T267, T269))
deleteC_in_gga(s(T281), tree(s(T281), T274, void), tree(s(T281), T276, void)) → U27_gga(T281, T274, T276, lessA_in_g(T281))
U27_gga(T281, T274, T276, lessA_out_g(T281)) → deleteC_out_gga(s(T281), tree(s(T281), T274, void), tree(s(T281), T276, void))
U27_gga(T281, T274, T276, lessA_out_g(T281)) → U28_gga(T281, T274, T276, deleteC_in_gga(s(T281), T274, T276))
deleteC_in_gga(T292, tree(T292, T293, void), tree(T292, T293, T295)) → U29_gga(T292, T293, T295, pB_in_ga(T292, T295))
U29_gga(T292, T293, T295, pB_out_ga(T292, T295)) → deleteC_out_gga(T292, tree(T292, T293, void), tree(T292, T293, T295))
deleteC_in_gga(s(T305), tree(s(T305), T300, void), tree(s(T305), T300, T302)) → U30_gga(T305, T300, T302, lessA_in_g(T305))
U30_gga(T305, T300, T302, lessA_out_g(T305)) → deleteC_out_gga(s(T305), tree(s(T305), T300, void), tree(s(T305), T300, T302))
U30_gga(T305, T300, T302, lessA_out_g(T305)) → U31_gga(T305, T300, T302, deleteC_in_gga(s(T305), void, T302))
deleteC_in_gga(T313, tree(T313, T314, tree(T328, void, T329)), tree(T328, T314, T329)) → deleteC_out_gga(T313, tree(T313, T314, tree(T328, void, T329)), tree(T328, T314, T329))
deleteC_in_gga(T313, tree(T313, T314, tree(T354, T355, T356)), tree(T360, T314, tree(T354, T361, T359))) → U32_gga(T313, T314, T354, T355, T356, T360, T361, T359, delminE_in_gaa(T355, T360, T361))
U32_gga(T313, T314, T354, T355, T356, T360, T361, T359, delminE_out_gaa(T355, T360, T361)) → deleteC_out_gga(T313, tree(T313, T314, tree(T354, T355, T356)), tree(T360, T314, tree(T354, T361, T359)))
deleteC_in_gga(T382, tree(T382, T383, T384), tree(T382, T386, T384)) → U33_gga(T382, T383, T384, T386, lessA_in_g(T382))
U33_gga(T382, T383, T384, T386, lessA_out_g(T382)) → deleteC_out_gga(T382, tree(T382, T383, T384), tree(T382, T386, T384))
U33_gga(T382, T383, T384, T386, lessA_out_g(T382)) → U34_gga(T382, T383, T384, T386, deleteC_in_gga(T382, T383, T386))
deleteC_in_gga(T399, tree(T399, T400, T401), tree(T399, T400, T403)) → U35_gga(T399, T400, T401, T403, lessA_in_g(T399))
U35_gga(T399, T400, T401, T403, lessA_out_g(T399)) → deleteC_out_gga(T399, tree(T399, T400, T401), tree(T399, T400, T403))
U35_gga(T399, T400, T401, T403, lessA_out_g(T399)) → U36_gga(T399, T400, T401, T403, deleteC_in_gga(T399, T401, T403))
deleteC_in_gga(0, tree(s(T423), T415, T416), tree(s(T423), T418, T416)) → U37_gga(T423, T415, T416, T418, deleteC_in_gga(0, T415, T418))
deleteC_in_gga(s(T434), tree(s(T435), T415, T416), tree(s(T435), T418, T416)) → U38_gga(T434, T435, T415, T416, T418, lessH_in_gg(T434, T435))
lessH_in_gg(0, s(T444)) → lessH_out_gg(0, s(T444))
lessH_in_gg(s(0), s(s(T457))) → lessH_out_gg(s(0), s(s(T457)))
lessH_in_gg(s(s(0)), s(s(s(T470)))) → lessH_out_gg(s(s(0)), s(s(s(T470))))
lessH_in_gg(s(s(s(0))), s(s(s(s(T483))))) → lessH_out_gg(s(s(s(0))), s(s(s(s(T483)))))
lessH_in_gg(s(s(s(s(0)))), s(s(s(s(s(T496)))))) → lessH_out_gg(s(s(s(s(0)))), s(s(s(s(s(T496))))))
lessH_in_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T509))))))) → lessH_out_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T509)))))))
lessH_in_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T522)))))))) → lessH_out_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T522))))))))
lessH_in_gg(s(s(s(s(s(s(s(T527))))))), s(s(s(s(s(s(s(T528)))))))) → U10_gg(T527, T528, lessG_in_gg(T527, T528))
lessG_in_gg(0, s(T539)) → lessG_out_gg(0, s(T539))
lessG_in_gg(s(T544), s(T545)) → U9_gg(T544, T545, lessG_in_gg(T544, T545))
U9_gg(T544, T545, lessG_out_gg(T544, T545)) → lessG_out_gg(s(T544), s(T545))
U10_gg(T527, T528, lessG_out_gg(T527, T528)) → lessH_out_gg(s(s(s(s(s(s(s(T527))))))), s(s(s(s(s(s(s(T528))))))))
U38_gga(T434, T435, T415, T416, T418, lessH_out_gg(T434, T435)) → deleteC_out_gga(s(T434), tree(s(T435), T415, T416), tree(s(T435), T418, T416))
U38_gga(T434, T435, T415, T416, T418, lessH_out_gg(T434, T435)) → U39_gga(T434, T435, T415, T416, T418, deleteC_in_gga(s(T434), T415, T418))
deleteC_in_gga(T562, tree(T563, T564, T565), tree(T563, T564, T567)) → U40_gga(T562, T563, T564, T565, T567, lessG_in_gg(T563, T562))
U40_gga(T562, T563, T564, T565, T567, lessG_out_gg(T563, T562)) → deleteC_out_gga(T562, tree(T563, T564, T565), tree(T563, T564, T567))
U40_gga(T562, T563, T564, T565, T567, lessG_out_gg(T563, T562)) → U41_gga(T562, T563, T564, T565, T567, deleteC_in_gga(T562, T565, T567))
deleteC_in_gga(s(T591), tree(0, T583, T584), tree(0, T583, T586)) → U42_gga(T591, T583, T584, T586, deleteC_in_gga(s(T591), T584, T586))
deleteC_in_gga(s(T601), tree(s(T600), T583, T584), tree(s(T600), T583, T586)) → U43_gga(T601, T600, T583, T584, T586, lessG_in_gg(T600, T601))
U43_gga(T601, T600, T583, T584, T586, lessG_out_gg(T600, T601)) → deleteC_out_gga(s(T601), tree(s(T600), T583, T584), tree(s(T600), T583, T586))
U43_gga(T601, T600, T583, T584, T586, lessG_out_gg(T600, T601)) → U44_gga(T601, T600, T583, T584, T586, deleteC_in_gga(s(T601), T584, T586))
U44_gga(T601, T600, T583, T584, T586, deleteC_out_gga(s(T601), T584, T586)) → deleteC_out_gga(s(T601), tree(s(T600), T583, T584), tree(s(T600), T583, T586))
U42_gga(T591, T583, T584, T586, deleteC_out_gga(s(T591), T584, T586)) → deleteC_out_gga(s(T591), tree(0, T583, T584), tree(0, T583, T586))
U41_gga(T562, T563, T564, T565, T567, deleteC_out_gga(T562, T565, T567)) → deleteC_out_gga(T562, tree(T563, T564, T565), tree(T563, T564, T567))
U39_gga(T434, T435, T415, T416, T418, deleteC_out_gga(s(T434), T415, T418)) → deleteC_out_gga(s(T434), tree(s(T435), T415, T416), tree(s(T435), T418, T416))
U37_gga(T423, T415, T416, T418, deleteC_out_gga(0, T415, T418)) → deleteC_out_gga(0, tree(s(T423), T415, T416), tree(s(T423), T418, T416))
U36_gga(T399, T400, T401, T403, deleteC_out_gga(T399, T401, T403)) → deleteC_out_gga(T399, tree(T399, T400, T401), tree(T399, T400, T403))
U34_gga(T382, T383, T384, T386, deleteC_out_gga(T382, T383, T386)) → deleteC_out_gga(T382, tree(T382, T383, T384), tree(T382, T386, T384))
U31_gga(T305, T300, T302, deleteC_out_gga(s(T305), void, T302)) → deleteC_out_gga(s(T305), tree(s(T305), T300, void), tree(s(T305), T300, T302))
U28_gga(T281, T274, T276, deleteC_out_gga(s(T281), T274, T276)) → deleteC_out_gga(s(T281), tree(s(T281), T274, void), tree(s(T281), T276, void))
U25_gga(T252, T253, T255, deleteC_out_gga(T252, T253, T255)) → deleteC_out_gga(T252, tree(T252, T253, void), tree(T252, T255, void))
U23_gga(T221, T216, T218, deleteC_out_gga(s(T221), T216, T218)) → deleteC_out_gga(s(T221), tree(s(T221), void, T216), tree(s(T221), void, T218))
U20_gga(T199, T192, T194, deleteC_out_gga(s(T199), void, T194)) → deleteC_out_gga(s(T199), tree(s(T199), void, T192), tree(s(T199), T194, T192))
U8_gga(T180, T181, T183, deleteC_out_gga(T180, T181, T183)) → pF_out_gga(T180, T181, T183)
U18_gga(T180, T181, T183, pF_out_gga(T180, T181, T183)) → deleteC_out_gga(T180, tree(T180, void, T181), tree(T180, void, T183))
U5_ga(T50, T45, deleteC_out_gga(s(T50), void, T45)) → pD_out_ga(T50, T45)
U13_gga(T50, T45, pD_out_ga(T50, T45)) → deleteC_out_gga(s(T50), tree(s(T50), void, void), tree(s(T50), T45, void))
U3_ga(T26, T28, deleteC_out_gga(T26, void, T28)) → pB_out_ga(T26, T28)
U11_gga(T26, T28, pB_out_ga(T26, T28)) → deleteC_out_gga(T26, tree(T26, void, void), tree(T26, T28, void))

The argument filtering Pi contains the following mapping:
deleteC_in_gga(x1, x2, x3)  =  deleteC_in_gga(x1, x2)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
void  =  void
deleteC_out_gga(x1, x2, x3)  =  deleteC_out_gga
U11_gga(x1, x2, x3)  =  U11_gga(x3)
pB_in_ga(x1, x2)  =  pB_in_ga(x1)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
lessA_in_g(x1)  =  lessA_in_g(x1)
s(x1)  =  s(x1)
U1_g(x1, x2)  =  U1_g(x2)
lessA_out_g(x1)  =  lessA_out_g
pB_out_ga(x1, x2)  =  pB_out_ga
U3_ga(x1, x2, x3)  =  U3_ga(x3)
U12_gga(x1, x2, x3)  =  U12_gga(x3)
U13_gga(x1, x2, x3)  =  U13_gga(x3)
pD_in_ga(x1, x2)  =  pD_in_ga(x1)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
pD_out_ga(x1, x2)  =  pD_out_ga
U5_ga(x1, x2, x3)  =  U5_ga(x3)
U14_gga(x1, x2, x3)  =  U14_gga(x3)
U15_gga(x1, x2, x3)  =  U15_gga(x3)
U16_gga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U16_gga(x8)
delminE_in_gaa(x1, x2, x3)  =  delminE_in_gaa(x1)
delminE_out_gaa(x1, x2, x3)  =  delminE_out_gaa(x2)
U6_gaa(x1, x2, x3, x4, x5, x6, x7)  =  U6_gaa(x7)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x4)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x4)
pF_in_gga(x1, x2, x3)  =  pF_in_gga(x1, x2)
U7_gga(x1, x2, x3, x4)  =  U7_gga(x1, x2, x4)
pF_out_gga(x1, x2, x3)  =  pF_out_gga
U8_gga(x1, x2, x3, x4)  =  U8_gga(x4)
U19_gga(x1, x2, x3, x4)  =  U19_gga(x1, x4)
U20_gga(x1, x2, x3, x4)  =  U20_gga(x4)
U21_gga(x1, x2, x3, x4)  =  U21_gga(x4)
U22_gga(x1, x2, x3, x4)  =  U22_gga(x1, x2, x4)
U23_gga(x1, x2, x3, x4)  =  U23_gga(x4)
U24_gga(x1, x2, x3, x4)  =  U24_gga(x1, x2, x4)
U25_gga(x1, x2, x3, x4)  =  U25_gga(x4)
U26_gga(x1, x2, x3, x4)  =  U26_gga(x4)
U27_gga(x1, x2, x3, x4)  =  U27_gga(x1, x2, x4)
U28_gga(x1, x2, x3, x4)  =  U28_gga(x4)
U29_gga(x1, x2, x3, x4)  =  U29_gga(x4)
U30_gga(x1, x2, x3, x4)  =  U30_gga(x1, x4)
U31_gga(x1, x2, x3, x4)  =  U31_gga(x4)
U32_gga(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U32_gga(x9)
U33_gga(x1, x2, x3, x4, x5)  =  U33_gga(x1, x2, x5)
U34_gga(x1, x2, x3, x4, x5)  =  U34_gga(x5)
U35_gga(x1, x2, x3, x4, x5)  =  U35_gga(x1, x3, x5)
U36_gga(x1, x2, x3, x4, x5)  =  U36_gga(x5)
0  =  0
U37_gga(x1, x2, x3, x4, x5)  =  U37_gga(x5)
U38_gga(x1, x2, x3, x4, x5, x6)  =  U38_gga(x1, x3, x6)
lessH_in_gg(x1, x2)  =  lessH_in_gg(x1, x2)
lessH_out_gg(x1, x2)  =  lessH_out_gg
U10_gg(x1, x2, x3)  =  U10_gg(x3)
lessG_in_gg(x1, x2)  =  lessG_in_gg(x1, x2)
lessG_out_gg(x1, x2)  =  lessG_out_gg
U9_gg(x1, x2, x3)  =  U9_gg(x3)
U39_gga(x1, x2, x3, x4, x5, x6)  =  U39_gga(x6)
U40_gga(x1, x2, x3, x4, x5, x6)  =  U40_gga(x1, x4, x6)
U41_gga(x1, x2, x3, x4, x5, x6)  =  U41_gga(x6)
U42_gga(x1, x2, x3, x4, x5)  =  U42_gga(x5)
U43_gga(x1, x2, x3, x4, x5, x6)  =  U43_gga(x1, x4, x6)
U44_gga(x1, x2, x3, x4, x5, x6)  =  U44_gga(x6)
LESSA_IN_G(x1)  =  LESSA_IN_G(x1)

We have to consider all (P,R,Pi)-chains

(24) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(25) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

LESSA_IN_G(s(T31)) → LESSA_IN_G(T31)

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains

(26) PiDPToQDPProof (EQUIVALENT transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(27) Obligation:

Q DP problem:
The TRS P consists of the following rules:

LESSA_IN_G(s(T31)) → LESSA_IN_G(T31)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(28) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • LESSA_IN_G(s(T31)) → LESSA_IN_G(T31)
    The graph contains the following edges 1 > 1

(29) YES

(30) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

DELETEC_IN_GGA(T180, tree(T180, void, T181), tree(T180, void, T183)) → PF_IN_GGA(T180, T181, T183)
PF_IN_GGA(T180, T181, T183) → U7_GGA(T180, T181, T183, lessA_in_g(T180))
U7_GGA(T180, T181, T183, lessA_out_g(T180)) → DELETEC_IN_GGA(T180, T181, T183)
DELETEC_IN_GGA(s(T221), tree(s(T221), void, T216), tree(s(T221), void, T218)) → U22_GGA(T221, T216, T218, lessA_in_g(T221))
U22_GGA(T221, T216, T218, lessA_out_g(T221)) → DELETEC_IN_GGA(s(T221), T216, T218)
DELETEC_IN_GGA(T252, tree(T252, T253, void), tree(T252, T255, void)) → U24_GGA(T252, T253, T255, lessA_in_g(T252))
U24_GGA(T252, T253, T255, lessA_out_g(T252)) → DELETEC_IN_GGA(T252, T253, T255)
DELETEC_IN_GGA(s(T281), tree(s(T281), T274, void), tree(s(T281), T276, void)) → U27_GGA(T281, T274, T276, lessA_in_g(T281))
U27_GGA(T281, T274, T276, lessA_out_g(T281)) → DELETEC_IN_GGA(s(T281), T274, T276)
DELETEC_IN_GGA(T382, tree(T382, T383, T384), tree(T382, T386, T384)) → U33_GGA(T382, T383, T384, T386, lessA_in_g(T382))
U33_GGA(T382, T383, T384, T386, lessA_out_g(T382)) → DELETEC_IN_GGA(T382, T383, T386)
DELETEC_IN_GGA(T399, tree(T399, T400, T401), tree(T399, T400, T403)) → U35_GGA(T399, T400, T401, T403, lessA_in_g(T399))
U35_GGA(T399, T400, T401, T403, lessA_out_g(T399)) → DELETEC_IN_GGA(T399, T401, T403)
DELETEC_IN_GGA(0, tree(s(T423), T415, T416), tree(s(T423), T418, T416)) → DELETEC_IN_GGA(0, T415, T418)
DELETEC_IN_GGA(T562, tree(T563, T564, T565), tree(T563, T564, T567)) → U40_GGA(T562, T563, T564, T565, T567, lessG_in_gg(T563, T562))
U40_GGA(T562, T563, T564, T565, T567, lessG_out_gg(T563, T562)) → DELETEC_IN_GGA(T562, T565, T567)
DELETEC_IN_GGA(s(T434), tree(s(T435), T415, T416), tree(s(T435), T418, T416)) → U38_GGA(T434, T435, T415, T416, T418, lessH_in_gg(T434, T435))
U38_GGA(T434, T435, T415, T416, T418, lessH_out_gg(T434, T435)) → DELETEC_IN_GGA(s(T434), T415, T418)
DELETEC_IN_GGA(s(T591), tree(0, T583, T584), tree(0, T583, T586)) → DELETEC_IN_GGA(s(T591), T584, T586)
DELETEC_IN_GGA(s(T601), tree(s(T600), T583, T584), tree(s(T600), T583, T586)) → U43_GGA(T601, T600, T583, T584, T586, lessG_in_gg(T600, T601))
U43_GGA(T601, T600, T583, T584, T586, lessG_out_gg(T600, T601)) → DELETEC_IN_GGA(s(T601), T584, T586)

The TRS R consists of the following rules:

deleteC_in_gga(T6, tree(T6, void, T7), T7) → deleteC_out_gga(T6, tree(T6, void, T7), T7)
deleteC_in_gga(T9, tree(T9, void, void), void) → deleteC_out_gga(T9, tree(T9, void, void), void)
deleteC_in_gga(T26, tree(T26, void, void), tree(T26, T28, void)) → U11_gga(T26, T28, pB_in_ga(T26, T28))
pB_in_ga(T26, T28) → U2_ga(T26, T28, lessA_in_g(T26))
lessA_in_g(s(T31)) → U1_g(T31, lessA_in_g(T31))
U1_g(T31, lessA_out_g(T31)) → lessA_out_g(s(T31))
U2_ga(T26, T28, lessA_out_g(T26)) → pB_out_ga(T26, T28)
U2_ga(T26, T28, lessA_out_g(T26)) → U3_ga(T26, T28, deleteC_in_gga(T26, void, T28))
deleteC_in_gga(T38, tree(T38, void, void), tree(T38, void, T40)) → U12_gga(T38, T40, pB_in_ga(T38, T40))
U12_gga(T38, T40, pB_out_ga(T38, T40)) → deleteC_out_gga(T38, tree(T38, void, void), tree(T38, void, T40))
deleteC_in_gga(s(T50), tree(s(T50), void, void), tree(s(T50), T45, void)) → U13_gga(T50, T45, pD_in_ga(T50, T45))
pD_in_ga(T50, T45) → U4_ga(T50, T45, lessA_in_g(T50))
U4_ga(T50, T45, lessA_out_g(T50)) → pD_out_ga(T50, T45)
U4_ga(T50, T45, lessA_out_g(T50)) → U5_ga(T50, T45, deleteC_in_gga(s(T50), void, T45))
deleteC_in_gga(T57, tree(T57, void, void), tree(T57, void, T59)) → U14_gga(T57, T59, pB_in_ga(T57, T59))
U14_gga(T57, T59, pB_out_ga(T57, T59)) → deleteC_out_gga(T57, tree(T57, void, void), tree(T57, void, T59))
deleteC_in_gga(s(T67), tree(s(T67), void, void), tree(s(T67), void, T64)) → U15_gga(T67, T64, pD_in_ga(T67, T64))
U15_gga(T67, T64, pD_out_ga(T67, T64)) → deleteC_out_gga(s(T67), tree(s(T67), void, void), tree(s(T67), void, T64))
deleteC_in_gga(T72, tree(T72, void, tree(T86, void, T87)), tree(T86, void, T87)) → deleteC_out_gga(T72, tree(T72, void, tree(T86, void, T87)), tree(T86, void, T87))
deleteC_in_gga(T72, tree(T72, void, tree(T112, T113, T114)), tree(T118, void, tree(T112, T119, T117))) → U16_gga(T72, T112, T113, T114, T118, T119, T117, delminE_in_gaa(T113, T118, T119))
delminE_in_gaa(tree(T132, void, T133), T132, T133) → delminE_out_gaa(tree(T132, void, T133), T132, T133)
delminE_in_gaa(tree(T146, T147, T148), T152, tree(T146, T153, T151)) → U6_gaa(T146, T147, T148, T152, T153, T151, delminE_in_gaa(T147, T152, T153))
U6_gaa(T146, T147, T148, T152, T153, T151, delminE_out_gaa(T147, T152, T153)) → delminE_out_gaa(tree(T146, T147, T148), T152, tree(T146, T153, T151))
U16_gga(T72, T112, T113, T114, T118, T119, T117, delminE_out_gaa(T113, T118, T119)) → deleteC_out_gga(T72, tree(T72, void, tree(T112, T113, T114)), tree(T118, void, tree(T112, T119, T117)))
deleteC_in_gga(T170, tree(T170, void, T171), tree(T170, T173, T171)) → U17_gga(T170, T171, T173, pB_in_ga(T170, T173))
U17_gga(T170, T171, T173, pB_out_ga(T170, T173)) → deleteC_out_gga(T170, tree(T170, void, T171), tree(T170, T173, T171))
deleteC_in_gga(T180, tree(T180, void, T181), tree(T180, void, T183)) → U18_gga(T180, T181, T183, pF_in_gga(T180, T181, T183))
pF_in_gga(T180, T181, T183) → U7_gga(T180, T181, T183, lessA_in_g(T180))
U7_gga(T180, T181, T183, lessA_out_g(T180)) → pF_out_gga(T180, T181, T183)
U7_gga(T180, T181, T183, lessA_out_g(T180)) → U8_gga(T180, T181, T183, deleteC_in_gga(T180, T181, T183))
deleteC_in_gga(s(T199), tree(s(T199), void, T192), tree(s(T199), T194, T192)) → U19_gga(T199, T192, T194, lessA_in_g(T199))
U19_gga(T199, T192, T194, lessA_out_g(T199)) → deleteC_out_gga(s(T199), tree(s(T199), void, T192), tree(s(T199), T194, T192))
U19_gga(T199, T192, T194, lessA_out_g(T199)) → U20_gga(T199, T192, T194, deleteC_in_gga(s(T199), void, T194))
deleteC_in_gga(T208, tree(T208, void, T209), tree(T208, void, T211)) → U21_gga(T208, T209, T211, pF_in_gga(T208, T209, T211))
U21_gga(T208, T209, T211, pF_out_gga(T208, T209, T211)) → deleteC_out_gga(T208, tree(T208, void, T209), tree(T208, void, T211))
deleteC_in_gga(s(T221), tree(s(T221), void, T216), tree(s(T221), void, T218)) → U22_gga(T221, T216, T218, lessA_in_g(T221))
U22_gga(T221, T216, T218, lessA_out_g(T221)) → deleteC_out_gga(s(T221), tree(s(T221), void, T216), tree(s(T221), void, T218))
U22_gga(T221, T216, T218, lessA_out_g(T221)) → U23_gga(T221, T216, T218, deleteC_in_gga(s(T221), T216, T218))
deleteC_in_gga(T228, tree(T228, T229, void), T229) → deleteC_out_gga(T228, tree(T228, T229, void), T229)
deleteC_in_gga(T252, tree(T252, T253, void), tree(T252, T255, void)) → U24_gga(T252, T253, T255, lessA_in_g(T252))
U24_gga(T252, T253, T255, lessA_out_g(T252)) → deleteC_out_gga(T252, tree(T252, T253, void), tree(T252, T255, void))
U24_gga(T252, T253, T255, lessA_out_g(T252)) → U25_gga(T252, T253, T255, deleteC_in_gga(T252, T253, T255))
deleteC_in_gga(T266, tree(T266, T267, void), tree(T266, T267, T269)) → U26_gga(T266, T267, T269, pB_in_ga(T266, T269))
U26_gga(T266, T267, T269, pB_out_ga(T266, T269)) → deleteC_out_gga(T266, tree(T266, T267, void), tree(T266, T267, T269))
deleteC_in_gga(s(T281), tree(s(T281), T274, void), tree(s(T281), T276, void)) → U27_gga(T281, T274, T276, lessA_in_g(T281))
U27_gga(T281, T274, T276, lessA_out_g(T281)) → deleteC_out_gga(s(T281), tree(s(T281), T274, void), tree(s(T281), T276, void))
U27_gga(T281, T274, T276, lessA_out_g(T281)) → U28_gga(T281, T274, T276, deleteC_in_gga(s(T281), T274, T276))
deleteC_in_gga(T292, tree(T292, T293, void), tree(T292, T293, T295)) → U29_gga(T292, T293, T295, pB_in_ga(T292, T295))
U29_gga(T292, T293, T295, pB_out_ga(T292, T295)) → deleteC_out_gga(T292, tree(T292, T293, void), tree(T292, T293, T295))
deleteC_in_gga(s(T305), tree(s(T305), T300, void), tree(s(T305), T300, T302)) → U30_gga(T305, T300, T302, lessA_in_g(T305))
U30_gga(T305, T300, T302, lessA_out_g(T305)) → deleteC_out_gga(s(T305), tree(s(T305), T300, void), tree(s(T305), T300, T302))
U30_gga(T305, T300, T302, lessA_out_g(T305)) → U31_gga(T305, T300, T302, deleteC_in_gga(s(T305), void, T302))
deleteC_in_gga(T313, tree(T313, T314, tree(T328, void, T329)), tree(T328, T314, T329)) → deleteC_out_gga(T313, tree(T313, T314, tree(T328, void, T329)), tree(T328, T314, T329))
deleteC_in_gga(T313, tree(T313, T314, tree(T354, T355, T356)), tree(T360, T314, tree(T354, T361, T359))) → U32_gga(T313, T314, T354, T355, T356, T360, T361, T359, delminE_in_gaa(T355, T360, T361))
U32_gga(T313, T314, T354, T355, T356, T360, T361, T359, delminE_out_gaa(T355, T360, T361)) → deleteC_out_gga(T313, tree(T313, T314, tree(T354, T355, T356)), tree(T360, T314, tree(T354, T361, T359)))
deleteC_in_gga(T382, tree(T382, T383, T384), tree(T382, T386, T384)) → U33_gga(T382, T383, T384, T386, lessA_in_g(T382))
U33_gga(T382, T383, T384, T386, lessA_out_g(T382)) → deleteC_out_gga(T382, tree(T382, T383, T384), tree(T382, T386, T384))
U33_gga(T382, T383, T384, T386, lessA_out_g(T382)) → U34_gga(T382, T383, T384, T386, deleteC_in_gga(T382, T383, T386))
deleteC_in_gga(T399, tree(T399, T400, T401), tree(T399, T400, T403)) → U35_gga(T399, T400, T401, T403, lessA_in_g(T399))
U35_gga(T399, T400, T401, T403, lessA_out_g(T399)) → deleteC_out_gga(T399, tree(T399, T400, T401), tree(T399, T400, T403))
U35_gga(T399, T400, T401, T403, lessA_out_g(T399)) → U36_gga(T399, T400, T401, T403, deleteC_in_gga(T399, T401, T403))
deleteC_in_gga(0, tree(s(T423), T415, T416), tree(s(T423), T418, T416)) → U37_gga(T423, T415, T416, T418, deleteC_in_gga(0, T415, T418))
deleteC_in_gga(s(T434), tree(s(T435), T415, T416), tree(s(T435), T418, T416)) → U38_gga(T434, T435, T415, T416, T418, lessH_in_gg(T434, T435))
lessH_in_gg(0, s(T444)) → lessH_out_gg(0, s(T444))
lessH_in_gg(s(0), s(s(T457))) → lessH_out_gg(s(0), s(s(T457)))
lessH_in_gg(s(s(0)), s(s(s(T470)))) → lessH_out_gg(s(s(0)), s(s(s(T470))))
lessH_in_gg(s(s(s(0))), s(s(s(s(T483))))) → lessH_out_gg(s(s(s(0))), s(s(s(s(T483)))))
lessH_in_gg(s(s(s(s(0)))), s(s(s(s(s(T496)))))) → lessH_out_gg(s(s(s(s(0)))), s(s(s(s(s(T496))))))
lessH_in_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T509))))))) → lessH_out_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T509)))))))
lessH_in_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T522)))))))) → lessH_out_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T522))))))))
lessH_in_gg(s(s(s(s(s(s(s(T527))))))), s(s(s(s(s(s(s(T528)))))))) → U10_gg(T527, T528, lessG_in_gg(T527, T528))
lessG_in_gg(0, s(T539)) → lessG_out_gg(0, s(T539))
lessG_in_gg(s(T544), s(T545)) → U9_gg(T544, T545, lessG_in_gg(T544, T545))
U9_gg(T544, T545, lessG_out_gg(T544, T545)) → lessG_out_gg(s(T544), s(T545))
U10_gg(T527, T528, lessG_out_gg(T527, T528)) → lessH_out_gg(s(s(s(s(s(s(s(T527))))))), s(s(s(s(s(s(s(T528))))))))
U38_gga(T434, T435, T415, T416, T418, lessH_out_gg(T434, T435)) → deleteC_out_gga(s(T434), tree(s(T435), T415, T416), tree(s(T435), T418, T416))
U38_gga(T434, T435, T415, T416, T418, lessH_out_gg(T434, T435)) → U39_gga(T434, T435, T415, T416, T418, deleteC_in_gga(s(T434), T415, T418))
deleteC_in_gga(T562, tree(T563, T564, T565), tree(T563, T564, T567)) → U40_gga(T562, T563, T564, T565, T567, lessG_in_gg(T563, T562))
U40_gga(T562, T563, T564, T565, T567, lessG_out_gg(T563, T562)) → deleteC_out_gga(T562, tree(T563, T564, T565), tree(T563, T564, T567))
U40_gga(T562, T563, T564, T565, T567, lessG_out_gg(T563, T562)) → U41_gga(T562, T563, T564, T565, T567, deleteC_in_gga(T562, T565, T567))
deleteC_in_gga(s(T591), tree(0, T583, T584), tree(0, T583, T586)) → U42_gga(T591, T583, T584, T586, deleteC_in_gga(s(T591), T584, T586))
deleteC_in_gga(s(T601), tree(s(T600), T583, T584), tree(s(T600), T583, T586)) → U43_gga(T601, T600, T583, T584, T586, lessG_in_gg(T600, T601))
U43_gga(T601, T600, T583, T584, T586, lessG_out_gg(T600, T601)) → deleteC_out_gga(s(T601), tree(s(T600), T583, T584), tree(s(T600), T583, T586))
U43_gga(T601, T600, T583, T584, T586, lessG_out_gg(T600, T601)) → U44_gga(T601, T600, T583, T584, T586, deleteC_in_gga(s(T601), T584, T586))
U44_gga(T601, T600, T583, T584, T586, deleteC_out_gga(s(T601), T584, T586)) → deleteC_out_gga(s(T601), tree(s(T600), T583, T584), tree(s(T600), T583, T586))
U42_gga(T591, T583, T584, T586, deleteC_out_gga(s(T591), T584, T586)) → deleteC_out_gga(s(T591), tree(0, T583, T584), tree(0, T583, T586))
U41_gga(T562, T563, T564, T565, T567, deleteC_out_gga(T562, T565, T567)) → deleteC_out_gga(T562, tree(T563, T564, T565), tree(T563, T564, T567))
U39_gga(T434, T435, T415, T416, T418, deleteC_out_gga(s(T434), T415, T418)) → deleteC_out_gga(s(T434), tree(s(T435), T415, T416), tree(s(T435), T418, T416))
U37_gga(T423, T415, T416, T418, deleteC_out_gga(0, T415, T418)) → deleteC_out_gga(0, tree(s(T423), T415, T416), tree(s(T423), T418, T416))
U36_gga(T399, T400, T401, T403, deleteC_out_gga(T399, T401, T403)) → deleteC_out_gga(T399, tree(T399, T400, T401), tree(T399, T400, T403))
U34_gga(T382, T383, T384, T386, deleteC_out_gga(T382, T383, T386)) → deleteC_out_gga(T382, tree(T382, T383, T384), tree(T382, T386, T384))
U31_gga(T305, T300, T302, deleteC_out_gga(s(T305), void, T302)) → deleteC_out_gga(s(T305), tree(s(T305), T300, void), tree(s(T305), T300, T302))
U28_gga(T281, T274, T276, deleteC_out_gga(s(T281), T274, T276)) → deleteC_out_gga(s(T281), tree(s(T281), T274, void), tree(s(T281), T276, void))
U25_gga(T252, T253, T255, deleteC_out_gga(T252, T253, T255)) → deleteC_out_gga(T252, tree(T252, T253, void), tree(T252, T255, void))
U23_gga(T221, T216, T218, deleteC_out_gga(s(T221), T216, T218)) → deleteC_out_gga(s(T221), tree(s(T221), void, T216), tree(s(T221), void, T218))
U20_gga(T199, T192, T194, deleteC_out_gga(s(T199), void, T194)) → deleteC_out_gga(s(T199), tree(s(T199), void, T192), tree(s(T199), T194, T192))
U8_gga(T180, T181, T183, deleteC_out_gga(T180, T181, T183)) → pF_out_gga(T180, T181, T183)
U18_gga(T180, T181, T183, pF_out_gga(T180, T181, T183)) → deleteC_out_gga(T180, tree(T180, void, T181), tree(T180, void, T183))
U5_ga(T50, T45, deleteC_out_gga(s(T50), void, T45)) → pD_out_ga(T50, T45)
U13_gga(T50, T45, pD_out_ga(T50, T45)) → deleteC_out_gga(s(T50), tree(s(T50), void, void), tree(s(T50), T45, void))
U3_ga(T26, T28, deleteC_out_gga(T26, void, T28)) → pB_out_ga(T26, T28)
U11_gga(T26, T28, pB_out_ga(T26, T28)) → deleteC_out_gga(T26, tree(T26, void, void), tree(T26, T28, void))

The argument filtering Pi contains the following mapping:
deleteC_in_gga(x1, x2, x3)  =  deleteC_in_gga(x1, x2)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
void  =  void
deleteC_out_gga(x1, x2, x3)  =  deleteC_out_gga
U11_gga(x1, x2, x3)  =  U11_gga(x3)
pB_in_ga(x1, x2)  =  pB_in_ga(x1)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
lessA_in_g(x1)  =  lessA_in_g(x1)
s(x1)  =  s(x1)
U1_g(x1, x2)  =  U1_g(x2)
lessA_out_g(x1)  =  lessA_out_g
pB_out_ga(x1, x2)  =  pB_out_ga
U3_ga(x1, x2, x3)  =  U3_ga(x3)
U12_gga(x1, x2, x3)  =  U12_gga(x3)
U13_gga(x1, x2, x3)  =  U13_gga(x3)
pD_in_ga(x1, x2)  =  pD_in_ga(x1)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
pD_out_ga(x1, x2)  =  pD_out_ga
U5_ga(x1, x2, x3)  =  U5_ga(x3)
U14_gga(x1, x2, x3)  =  U14_gga(x3)
U15_gga(x1, x2, x3)  =  U15_gga(x3)
U16_gga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U16_gga(x8)
delminE_in_gaa(x1, x2, x3)  =  delminE_in_gaa(x1)
delminE_out_gaa(x1, x2, x3)  =  delminE_out_gaa(x2)
U6_gaa(x1, x2, x3, x4, x5, x6, x7)  =  U6_gaa(x7)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x4)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x4)
pF_in_gga(x1, x2, x3)  =  pF_in_gga(x1, x2)
U7_gga(x1, x2, x3, x4)  =  U7_gga(x1, x2, x4)
pF_out_gga(x1, x2, x3)  =  pF_out_gga
U8_gga(x1, x2, x3, x4)  =  U8_gga(x4)
U19_gga(x1, x2, x3, x4)  =  U19_gga(x1, x4)
U20_gga(x1, x2, x3, x4)  =  U20_gga(x4)
U21_gga(x1, x2, x3, x4)  =  U21_gga(x4)
U22_gga(x1, x2, x3, x4)  =  U22_gga(x1, x2, x4)
U23_gga(x1, x2, x3, x4)  =  U23_gga(x4)
U24_gga(x1, x2, x3, x4)  =  U24_gga(x1, x2, x4)
U25_gga(x1, x2, x3, x4)  =  U25_gga(x4)
U26_gga(x1, x2, x3, x4)  =  U26_gga(x4)
U27_gga(x1, x2, x3, x4)  =  U27_gga(x1, x2, x4)
U28_gga(x1, x2, x3, x4)  =  U28_gga(x4)
U29_gga(x1, x2, x3, x4)  =  U29_gga(x4)
U30_gga(x1, x2, x3, x4)  =  U30_gga(x1, x4)
U31_gga(x1, x2, x3, x4)  =  U31_gga(x4)
U32_gga(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U32_gga(x9)
U33_gga(x1, x2, x3, x4, x5)  =  U33_gga(x1, x2, x5)
U34_gga(x1, x2, x3, x4, x5)  =  U34_gga(x5)
U35_gga(x1, x2, x3, x4, x5)  =  U35_gga(x1, x3, x5)
U36_gga(x1, x2, x3, x4, x5)  =  U36_gga(x5)
0  =  0
U37_gga(x1, x2, x3, x4, x5)  =  U37_gga(x5)
U38_gga(x1, x2, x3, x4, x5, x6)  =  U38_gga(x1, x3, x6)
lessH_in_gg(x1, x2)  =  lessH_in_gg(x1, x2)
lessH_out_gg(x1, x2)  =  lessH_out_gg
U10_gg(x1, x2, x3)  =  U10_gg(x3)
lessG_in_gg(x1, x2)  =  lessG_in_gg(x1, x2)
lessG_out_gg(x1, x2)  =  lessG_out_gg
U9_gg(x1, x2, x3)  =  U9_gg(x3)
U39_gga(x1, x2, x3, x4, x5, x6)  =  U39_gga(x6)
U40_gga(x1, x2, x3, x4, x5, x6)  =  U40_gga(x1, x4, x6)
U41_gga(x1, x2, x3, x4, x5, x6)  =  U41_gga(x6)
U42_gga(x1, x2, x3, x4, x5)  =  U42_gga(x5)
U43_gga(x1, x2, x3, x4, x5, x6)  =  U43_gga(x1, x4, x6)
U44_gga(x1, x2, x3, x4, x5, x6)  =  U44_gga(x6)
DELETEC_IN_GGA(x1, x2, x3)  =  DELETEC_IN_GGA(x1, x2)
PF_IN_GGA(x1, x2, x3)  =  PF_IN_GGA(x1, x2)
U7_GGA(x1, x2, x3, x4)  =  U7_GGA(x1, x2, x4)
U22_GGA(x1, x2, x3, x4)  =  U22_GGA(x1, x2, x4)
U24_GGA(x1, x2, x3, x4)  =  U24_GGA(x1, x2, x4)
U27_GGA(x1, x2, x3, x4)  =  U27_GGA(x1, x2, x4)
U33_GGA(x1, x2, x3, x4, x5)  =  U33_GGA(x1, x2, x5)
U35_GGA(x1, x2, x3, x4, x5)  =  U35_GGA(x1, x3, x5)
U38_GGA(x1, x2, x3, x4, x5, x6)  =  U38_GGA(x1, x3, x6)
U40_GGA(x1, x2, x3, x4, x5, x6)  =  U40_GGA(x1, x4, x6)
U43_GGA(x1, x2, x3, x4, x5, x6)  =  U43_GGA(x1, x4, x6)

We have to consider all (P,R,Pi)-chains

(31) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(32) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

DELETEC_IN_GGA(T180, tree(T180, void, T181), tree(T180, void, T183)) → PF_IN_GGA(T180, T181, T183)
PF_IN_GGA(T180, T181, T183) → U7_GGA(T180, T181, T183, lessA_in_g(T180))
U7_GGA(T180, T181, T183, lessA_out_g(T180)) → DELETEC_IN_GGA(T180, T181, T183)
DELETEC_IN_GGA(s(T221), tree(s(T221), void, T216), tree(s(T221), void, T218)) → U22_GGA(T221, T216, T218, lessA_in_g(T221))
U22_GGA(T221, T216, T218, lessA_out_g(T221)) → DELETEC_IN_GGA(s(T221), T216, T218)
DELETEC_IN_GGA(T252, tree(T252, T253, void), tree(T252, T255, void)) → U24_GGA(T252, T253, T255, lessA_in_g(T252))
U24_GGA(T252, T253, T255, lessA_out_g(T252)) → DELETEC_IN_GGA(T252, T253, T255)
DELETEC_IN_GGA(s(T281), tree(s(T281), T274, void), tree(s(T281), T276, void)) → U27_GGA(T281, T274, T276, lessA_in_g(T281))
U27_GGA(T281, T274, T276, lessA_out_g(T281)) → DELETEC_IN_GGA(s(T281), T274, T276)
DELETEC_IN_GGA(T382, tree(T382, T383, T384), tree(T382, T386, T384)) → U33_GGA(T382, T383, T384, T386, lessA_in_g(T382))
U33_GGA(T382, T383, T384, T386, lessA_out_g(T382)) → DELETEC_IN_GGA(T382, T383, T386)
DELETEC_IN_GGA(T399, tree(T399, T400, T401), tree(T399, T400, T403)) → U35_GGA(T399, T400, T401, T403, lessA_in_g(T399))
U35_GGA(T399, T400, T401, T403, lessA_out_g(T399)) → DELETEC_IN_GGA(T399, T401, T403)
DELETEC_IN_GGA(0, tree(s(T423), T415, T416), tree(s(T423), T418, T416)) → DELETEC_IN_GGA(0, T415, T418)
DELETEC_IN_GGA(T562, tree(T563, T564, T565), tree(T563, T564, T567)) → U40_GGA(T562, T563, T564, T565, T567, lessG_in_gg(T563, T562))
U40_GGA(T562, T563, T564, T565, T567, lessG_out_gg(T563, T562)) → DELETEC_IN_GGA(T562, T565, T567)
DELETEC_IN_GGA(s(T434), tree(s(T435), T415, T416), tree(s(T435), T418, T416)) → U38_GGA(T434, T435, T415, T416, T418, lessH_in_gg(T434, T435))
U38_GGA(T434, T435, T415, T416, T418, lessH_out_gg(T434, T435)) → DELETEC_IN_GGA(s(T434), T415, T418)
DELETEC_IN_GGA(s(T591), tree(0, T583, T584), tree(0, T583, T586)) → DELETEC_IN_GGA(s(T591), T584, T586)
DELETEC_IN_GGA(s(T601), tree(s(T600), T583, T584), tree(s(T600), T583, T586)) → U43_GGA(T601, T600, T583, T584, T586, lessG_in_gg(T600, T601))
U43_GGA(T601, T600, T583, T584, T586, lessG_out_gg(T600, T601)) → DELETEC_IN_GGA(s(T601), T584, T586)

The TRS R consists of the following rules:

lessA_in_g(s(T31)) → U1_g(T31, lessA_in_g(T31))
lessG_in_gg(0, s(T539)) → lessG_out_gg(0, s(T539))
lessG_in_gg(s(T544), s(T545)) → U9_gg(T544, T545, lessG_in_gg(T544, T545))
lessH_in_gg(0, s(T444)) → lessH_out_gg(0, s(T444))
lessH_in_gg(s(0), s(s(T457))) → lessH_out_gg(s(0), s(s(T457)))
lessH_in_gg(s(s(0)), s(s(s(T470)))) → lessH_out_gg(s(s(0)), s(s(s(T470))))
lessH_in_gg(s(s(s(0))), s(s(s(s(T483))))) → lessH_out_gg(s(s(s(0))), s(s(s(s(T483)))))
lessH_in_gg(s(s(s(s(0)))), s(s(s(s(s(T496)))))) → lessH_out_gg(s(s(s(s(0)))), s(s(s(s(s(T496))))))
lessH_in_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T509))))))) → lessH_out_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T509)))))))
lessH_in_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T522)))))))) → lessH_out_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T522))))))))
lessH_in_gg(s(s(s(s(s(s(s(T527))))))), s(s(s(s(s(s(s(T528)))))))) → U10_gg(T527, T528, lessG_in_gg(T527, T528))
U1_g(T31, lessA_out_g(T31)) → lessA_out_g(s(T31))
U9_gg(T544, T545, lessG_out_gg(T544, T545)) → lessG_out_gg(s(T544), s(T545))
U10_gg(T527, T528, lessG_out_gg(T527, T528)) → lessH_out_gg(s(s(s(s(s(s(s(T527))))))), s(s(s(s(s(s(s(T528))))))))

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
void  =  void
lessA_in_g(x1)  =  lessA_in_g(x1)
s(x1)  =  s(x1)
U1_g(x1, x2)  =  U1_g(x2)
lessA_out_g(x1)  =  lessA_out_g
0  =  0
lessH_in_gg(x1, x2)  =  lessH_in_gg(x1, x2)
lessH_out_gg(x1, x2)  =  lessH_out_gg
U10_gg(x1, x2, x3)  =  U10_gg(x3)
lessG_in_gg(x1, x2)  =  lessG_in_gg(x1, x2)
lessG_out_gg(x1, x2)  =  lessG_out_gg
U9_gg(x1, x2, x3)  =  U9_gg(x3)
DELETEC_IN_GGA(x1, x2, x3)  =  DELETEC_IN_GGA(x1, x2)
PF_IN_GGA(x1, x2, x3)  =  PF_IN_GGA(x1, x2)
U7_GGA(x1, x2, x3, x4)  =  U7_GGA(x1, x2, x4)
U22_GGA(x1, x2, x3, x4)  =  U22_GGA(x1, x2, x4)
U24_GGA(x1, x2, x3, x4)  =  U24_GGA(x1, x2, x4)
U27_GGA(x1, x2, x3, x4)  =  U27_GGA(x1, x2, x4)
U33_GGA(x1, x2, x3, x4, x5)  =  U33_GGA(x1, x2, x5)
U35_GGA(x1, x2, x3, x4, x5)  =  U35_GGA(x1, x3, x5)
U38_GGA(x1, x2, x3, x4, x5, x6)  =  U38_GGA(x1, x3, x6)
U40_GGA(x1, x2, x3, x4, x5, x6)  =  U40_GGA(x1, x4, x6)
U43_GGA(x1, x2, x3, x4, x5, x6)  =  U43_GGA(x1, x4, x6)

We have to consider all (P,R,Pi)-chains

(33) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(34) Obligation:

Q DP problem:
The TRS P consists of the following rules:

DELETEC_IN_GGA(T180, tree(T180, void, T181)) → PF_IN_GGA(T180, T181)
PF_IN_GGA(T180, T181) → U7_GGA(T180, T181, lessA_in_g(T180))
U7_GGA(T180, T181, lessA_out_g) → DELETEC_IN_GGA(T180, T181)
DELETEC_IN_GGA(s(T221), tree(s(T221), void, T216)) → U22_GGA(T221, T216, lessA_in_g(T221))
U22_GGA(T221, T216, lessA_out_g) → DELETEC_IN_GGA(s(T221), T216)
DELETEC_IN_GGA(T252, tree(T252, T253, void)) → U24_GGA(T252, T253, lessA_in_g(T252))
U24_GGA(T252, T253, lessA_out_g) → DELETEC_IN_GGA(T252, T253)
DELETEC_IN_GGA(s(T281), tree(s(T281), T274, void)) → U27_GGA(T281, T274, lessA_in_g(T281))
U27_GGA(T281, T274, lessA_out_g) → DELETEC_IN_GGA(s(T281), T274)
DELETEC_IN_GGA(T382, tree(T382, T383, T384)) → U33_GGA(T382, T383, lessA_in_g(T382))
U33_GGA(T382, T383, lessA_out_g) → DELETEC_IN_GGA(T382, T383)
DELETEC_IN_GGA(T399, tree(T399, T400, T401)) → U35_GGA(T399, T401, lessA_in_g(T399))
U35_GGA(T399, T401, lessA_out_g) → DELETEC_IN_GGA(T399, T401)
DELETEC_IN_GGA(0, tree(s(T423), T415, T416)) → DELETEC_IN_GGA(0, T415)
DELETEC_IN_GGA(T562, tree(T563, T564, T565)) → U40_GGA(T562, T565, lessG_in_gg(T563, T562))
U40_GGA(T562, T565, lessG_out_gg) → DELETEC_IN_GGA(T562, T565)
DELETEC_IN_GGA(s(T434), tree(s(T435), T415, T416)) → U38_GGA(T434, T415, lessH_in_gg(T434, T435))
U38_GGA(T434, T415, lessH_out_gg) → DELETEC_IN_GGA(s(T434), T415)
DELETEC_IN_GGA(s(T591), tree(0, T583, T584)) → DELETEC_IN_GGA(s(T591), T584)
DELETEC_IN_GGA(s(T601), tree(s(T600), T583, T584)) → U43_GGA(T601, T584, lessG_in_gg(T600, T601))
U43_GGA(T601, T584, lessG_out_gg) → DELETEC_IN_GGA(s(T601), T584)

The TRS R consists of the following rules:

lessA_in_g(s(T31)) → U1_g(lessA_in_g(T31))
lessG_in_gg(0, s(T539)) → lessG_out_gg
lessG_in_gg(s(T544), s(T545)) → U9_gg(lessG_in_gg(T544, T545))
lessH_in_gg(0, s(T444)) → lessH_out_gg
lessH_in_gg(s(0), s(s(T457))) → lessH_out_gg
lessH_in_gg(s(s(0)), s(s(s(T470)))) → lessH_out_gg
lessH_in_gg(s(s(s(0))), s(s(s(s(T483))))) → lessH_out_gg
lessH_in_gg(s(s(s(s(0)))), s(s(s(s(s(T496)))))) → lessH_out_gg
lessH_in_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T509))))))) → lessH_out_gg
lessH_in_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T522)))))))) → lessH_out_gg
lessH_in_gg(s(s(s(s(s(s(s(T527))))))), s(s(s(s(s(s(s(T528)))))))) → U10_gg(lessG_in_gg(T527, T528))
U1_g(lessA_out_g) → lessA_out_g
U9_gg(lessG_out_gg) → lessG_out_gg
U10_gg(lessG_out_gg) → lessH_out_gg

The set Q consists of the following terms:

lessA_in_g(x0)
lessG_in_gg(x0, x1)
lessH_in_gg(x0, x1)
U1_g(x0)
U9_gg(x0)
U10_gg(x0)

We have to consider all (P,Q,R)-chains.

(35) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • PF_IN_GGA(T180, T181) → U7_GGA(T180, T181, lessA_in_g(T180))
    The graph contains the following edges 1 >= 1, 2 >= 2

  • U7_GGA(T180, T181, lessA_out_g) → DELETEC_IN_GGA(T180, T181)
    The graph contains the following edges 1 >= 1, 2 >= 2

  • DELETEC_IN_GGA(T180, tree(T180, void, T181)) → PF_IN_GGA(T180, T181)
    The graph contains the following edges 1 >= 1, 2 > 1, 2 > 2

  • DELETEC_IN_GGA(s(T591), tree(0, T583, T584)) → DELETEC_IN_GGA(s(T591), T584)
    The graph contains the following edges 1 >= 1, 2 > 2

  • DELETEC_IN_GGA(0, tree(s(T423), T415, T416)) → DELETEC_IN_GGA(0, T415)
    The graph contains the following edges 1 >= 1, 2 > 2

  • U22_GGA(T221, T216, lessA_out_g) → DELETEC_IN_GGA(s(T221), T216)
    The graph contains the following edges 2 >= 2

  • DELETEC_IN_GGA(s(T221), tree(s(T221), void, T216)) → U22_GGA(T221, T216, lessA_in_g(T221))
    The graph contains the following edges 1 > 1, 2 > 1, 2 > 2

  • U24_GGA(T252, T253, lessA_out_g) → DELETEC_IN_GGA(T252, T253)
    The graph contains the following edges 1 >= 1, 2 >= 2

  • DELETEC_IN_GGA(T252, tree(T252, T253, void)) → U24_GGA(T252, T253, lessA_in_g(T252))
    The graph contains the following edges 1 >= 1, 2 > 1, 2 > 2

  • U27_GGA(T281, T274, lessA_out_g) → DELETEC_IN_GGA(s(T281), T274)
    The graph contains the following edges 2 >= 2

  • DELETEC_IN_GGA(s(T281), tree(s(T281), T274, void)) → U27_GGA(T281, T274, lessA_in_g(T281))
    The graph contains the following edges 1 > 1, 2 > 1, 2 > 2

  • U33_GGA(T382, T383, lessA_out_g) → DELETEC_IN_GGA(T382, T383)
    The graph contains the following edges 1 >= 1, 2 >= 2

  • DELETEC_IN_GGA(T382, tree(T382, T383, T384)) → U33_GGA(T382, T383, lessA_in_g(T382))
    The graph contains the following edges 1 >= 1, 2 > 1, 2 > 2

  • U35_GGA(T399, T401, lessA_out_g) → DELETEC_IN_GGA(T399, T401)
    The graph contains the following edges 1 >= 1, 2 >= 2

  • DELETEC_IN_GGA(T399, tree(T399, T400, T401)) → U35_GGA(T399, T401, lessA_in_g(T399))
    The graph contains the following edges 1 >= 1, 2 > 1, 2 > 2

  • U40_GGA(T562, T565, lessG_out_gg) → DELETEC_IN_GGA(T562, T565)
    The graph contains the following edges 1 >= 1, 2 >= 2

  • DELETEC_IN_GGA(T562, tree(T563, T564, T565)) → U40_GGA(T562, T565, lessG_in_gg(T563, T562))
    The graph contains the following edges 1 >= 1, 2 > 2

  • U38_GGA(T434, T415, lessH_out_gg) → DELETEC_IN_GGA(s(T434), T415)
    The graph contains the following edges 2 >= 2

  • U43_GGA(T601, T584, lessG_out_gg) → DELETEC_IN_GGA(s(T601), T584)
    The graph contains the following edges 2 >= 2

  • DELETEC_IN_GGA(s(T434), tree(s(T435), T415, T416)) → U38_GGA(T434, T415, lessH_in_gg(T434, T435))
    The graph contains the following edges 1 > 1, 2 > 2

  • DELETEC_IN_GGA(s(T601), tree(s(T600), T583, T584)) → U43_GGA(T601, T584, lessG_in_gg(T600, T601))
    The graph contains the following edges 1 > 1, 2 > 2

(36) YES